In: Proceedings of the SMC 2001, Tucson (AZ) USA, pages 2700-2705. October 2001.
Abstract: 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.