	US 11,906,943 B2
	Method for automatic translation of ladder logic to a SMT-based model checker in a network
Roberto Bruttomesso, Morazzone (IT); Alessandro Di Pinto, Malnate (IT); Moreno Carullo, Gavirate (IT); and Andrea Carcano, San Francisco, CA (US)
Assigned to Nozomi Networks Sagl, Mendrisio (CH)
Filed by Nozomi Networks Sagl, Mendrisio (CH)
Filed on Aug. 12, 2021, as Appl. No. 17/400,947.
Prior Publication US 2023/0059985 A1, Feb. 23, 2023
Int. Cl. G05B 19/05 (2006.01)

CPC G05B 19/054 (2013.01) [G05B 19/056 (2013.01); G05B 2219/1164 (2013.01); G05B 2219/13018 (2013.01); G05B 2219/13019 (2013.01); G05B 2219/15023 (2013.01)]

12 Claims

1. A method for automatic translation of ladder logic to a Satisfiability Modulo Theories based model checker in a network comprising:

defining (10) a topology of said network basing on packets exchanged in said network;

extracting (20) a program from said packets relating to a PLC in said network and identifying inputs, outputs, variables and a ladder diagram of said PLC;

translating (30) said inputs, outputs, variables and ladder diagram into a predefined formal model;

wherein said predefined formal model is an SMT-based model checker defined by a circuit with a global clock that divides an execution into discrete time steps;

and wherein said translating (30) comprises:

translating the set of data types of said program according to a predefined model set of data types of said circuit-like SMT-based model checker;

translating said inputs of said PLC as corresponding model inputs of said circuit-like SMT-based model checker;

translating said outputs of said PLC as corresponding model output latches of said SMT-based model checker;

translating said variables of said PLC as corresponding model variable latches of said SMT-based model checker;

translating comparators and arithmetic operators of said ladder diagram into a plurality of predefined model functions of said SMT-based model checker;

translating contacts and coils of said ladder diagram according to predefined model recursive procedures relating to said predefined model set of data types, said model inputs, said model output latches, said model variable latches and said plurality of predefined model functions, wherein said contacts are switches that can block or allow the flow of the current in a connection and each of said contacts is controlled by a Boolean input or variable, and wherein said coils are assignments to Boolean variables;

and wherein said SMT-based model checker defines a circuit with a global clock that divides the execution into discrete time steps;

wherein said SMT-based model checker comprises:

model inputs as basic signals of supported types that get a corresponding value at every time step;

model output latches and model variable latches as basic memory elements that can hold a value of a supported type;

Boolean gates;

predefined model functions as comparators and arithmetic operators;

constants as signal values of supported types that never change value at every of said time steps.