Importance

Loading Importance Indicators...

Abstract

The present invention is related to a method for checking correctness of a PLC program described by functional specifications typically presented as a timing chart. The method comprises: —S1: translating the PLC program into a model, —S2: translating the timing chart and integrating said timing chart into the model, —S3: computing abstract semantics, to infer information eventually missing in the timing chart, —S4: predicating transformation, and deducing properties to be verified, from the model and from predefined PLC formalized instructions, in order to satisfy timing chart verification, —S5: solving and checking whether said properties are always verified, or providing counter-examples, —S6: translating said counter-examples into PLC model errors events initial configurations, —S7: simulating execution, —S8: assembling states and events executions variables values, and —S9: translating back to PLC program.

Loading the Abstract Image...

First Claim