US 12,169,396 B2
Method for analyzing a Programmable Logic Controller program
Denis Cousineau, Rennes (FR)
Assigned to MITSUBISHI ELECTRIC CORPORATION, Tokyo (JP)
Appl. No. 17/788,625
Filed by Mitsubishi Electric Corporation, Tokyo (JP)
PCT Filed Dec. 23, 2020, PCT No. PCT/JP2020/049302
§ 371(c)(1), (2) Date Jun. 23, 2022,
PCT Pub. No. WO2021/199552, PCT Pub. Date Oct. 7, 2021.
Claims priority of application No. 20315085 (EP), filed on Mar. 31, 2020.
Prior Publication US 2023/0030253 A1, Feb. 2, 2023
Int. Cl. G05B 19/04 (2006.01); G05B 19/042 (2006.01); G06F 8/41 (2018.01)
CPC G05B 19/041 (2013.01) [G05B 19/042 (2013.01); G06F 8/42 (2013.01)] 10 Claims
OG exemplary drawing
 
1. A Programmable Logic Controller Program analysis method comprising the following steps:
translating an original program of the type of a Programmable Logic Controller Program, into a program model in a logical framework;
translating, based at least on said program model, user specifications into a specification model in a logical framework;
determining, from at least said program model and predefined language formalization, a set of properties on internal variables of said original program;
verifying, by an automated solver, satisfiability of said set of properties coupled with interlocking properties obtained from the specification model and providing, if contraposition of a property from said set of properties is satisfiable, a set of counter-examples representative of program model's inputs and internal memory values for which said property contraposition is satisfiable, or providing, if said set of properties is always satisfied, confirmation thereof;
translating counter-examples, into error initial configurations of said program model, said initial configurations comprising initial values of inputs and internal memory;
simulating the execution of the program model with error initial configurations of said program model, and recording error intermediary configurations of said program model simulation, from the beginning of execution up to said property violation, said intermediary configurations comprising intermediary values of internal memory;
translating error initial configurations of said program model and error intermediary configurations of said program model simulation, into error initial and intermediary configurations of said original program; and displaying said program error initial and intermediary configurations.