TM_GF_SMC2001_oct_2001

Mertke, T.; Frey, G.:
Formal Verification of PLC-programs generated from Signal Interpreted Petri Nets
Proceedings of the SMC 2001, Tucson (AZ) USA October 07-10, 2001, pp. 2700-2705.

This paper outlines an approach for applying model-checking to logic control algorithms in a way that is easy to understand and to apply by non-specialists. Non-specialists in this case means the designers of PLC programs (mostly control engineers and technicians) because they often have only restricted knowledge in computer science. A graphical design approach (based on Signal Interpreted Petri Nets, SIPN) is used to generate a controller for a benchmark problem. This controller is then checked against a set of semi-verbally formulated properties, and improved to fulfill them. The combination of the graphical SIPN design approach and the semi-verbal specification language results in a very transparent and easy to apply approach to the design and verification of PLC software.