For the most recent entries see the Petri Nets Newsletter.

Formal Verification of PLC-programs generated from Signal Interpreted Petri Nets.

Mertke, T.; Frey, G.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography