Formal verification of PLC programs generated from signal interpreted Petri nets

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