The first approach contains in implementing PLC programs directly in a formal language, and next is automatically to generate the PLC code. Introduces a program based on a set of rules to translate Time Interpreted Petri Nets (TIPN) control specifications into Ladder Diagrams. In a set of tools was presented for implementation of PLC programs using Signal Interpreted Petri Nets (SIPN), symbolic model checking was used for validation, verification and the control specification was implemented finally through Instruction List (IL). Introduces a formalism based on timed state machines called PLC-automata and a translation of this formalism into Structured Text (ST) code.
The second approach contains in translating the existing PLC programs into a formal language and performs the verification automatically. This approach permits the use of formal languages for the verification of PLC programs without changing the programming paradigm. Our work is based on this second approach. Some works using this approach have been developed. And provide a Petri Nets semantics for a subset of the IL language. To provide a framework for automatic verification of programs written in IL, a formal semantics is presented for a subset of the IL language, which is coded directly into a model-checking tool. It is then possible to verify behavioral properties automatically written in LTL. LD programs are presented formally through a transition system. In a combination of probabilistic testing and program analysis has been used to detect race conditions in relay ladder programs. Usually discusses the transformation between Net Condition Event System (NCES) State Charts and PLC languages.
The original PLC program is abstracted according to these properties before the generation of the timed automata, for each property to be verified it may be generated a different time automata. It uses a model checking framework to verify SFC programs and it suggests static analysis techniques to overcome semantic issues and a verification approach for IL and SFC programs.