METHOD AND APPARATUS FOR EXPRESSING AND VERIFYING FUNCTIONAL SPECIFICATIONS OF A PROGRAMMABLE LOGIC CONTROLLER PROGRAM

摘要

It is disclosed a PLC Program analysis method where a program (PROG) is translated (TRANS 1) into a program model (PMOD) in a logical framework, from which properties (Prop) are determined. Said properties coupled with interlocking properties (IntProp) are verified by an automated solver (SMT). If contraposition of a property (Prop) is satisfiable, counter-examples (PROOF NOK) representative of model's inputs and internal memory values is provided. Counter-examples (PROOF NOK) are translated into error initial configurations (IniConf) of said model. Execution of the model is simulated (EXE) with said model error initial configurations (IniConf), and error intermediary configurations (AST-IntConf) of said model simulation are recorded up to said property violation. Error initial and intermediary configurations (Lad-IniConf, Lad-IntConf) of said original program (PROG) are derived from error initial configurations (IniConf) of said model and error intermediary configurations (AST-IntConf) of said model simulation and displayed.;An apparatus for executing said method is provided.