A Petri Net based Approach to the Development of correct Logic Controllers
Stéphane Klein, Georg Frey, Lothar Litz · 2002
An overview on the different steps involved in the development of a logic control algorithm from the informal specification to the final implementation on a programmable logic controller (PLC) is given. Based on this overview the steps in the development process are presented in detail. An example is used throughout the paper to illustrate the methods. The approach uses Signal Interpreted Petri Nets for the formal description of control algorithms, symbolic model checking for Verification and Validation, and automatic code generation in Instruction List according to IEC 61131-3 for implementation.