The patent badge is an abbreviated version of the USPTO patent document. The patent badge does contain a link to the full patent document.
The patent badge is an abbreviated version of the USPTO patent document. The patent badge covers the following: Patent number, Date patent was issued, Date patent was filed, Title of the patent, Applicant, Inventor, Assignee, Attorney firm, Primary examiner, Assistant examiner, CPCs, and Abstract. The patent badge does contain a link to the full patent document (in Adobe Acrobat format, aka pdf). To download or print any patent click here.
Patent No.:
Date of Patent:
Sep. 10, 2024
Filed:
Feb. 07, 2020
Mitsubishi Electric Corporation, Tokyo, JP;
Denis Cousineau, Rennes, FR;
MITSUBISHI ELECTRIC CORPORATION, Tokyo, JP;
Abstract
It is disclosed a PLC Program analysis method where a program (PROG) is translated (TRANS) into a model (MOD) in a logical framework, from which properties (Prop) are determined. Said properties coupled with user specifications (IntProp) are verified by an automated solver (SMT). If contraposition of a property (Prop) is satisfiable, counter-examples (PROOF NOK) representative of model 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.