In: Proc. 2nd IMACS Symposium on Mathematical Modelling (MATHMOD VIENNA '97), Wien, Feb. 1997, pages 171-176. 1997. Available at http://www.informatik.tu-cottbus.de/~wwwdssz/publications/papers.html.
Abstract: The development of provably error-free concurrent systems is still a challenge of practical system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well-known approaches using formal methods. Among those Petri net analysis techniques suitable for strong verification purposes there is an increasing amount of promising methods avoiding the construction of the complete interleaving state space, and by this way the well-known state explosion problem. This paper claims to demonstrate that the available methods and tools are actually applicable successfully to at least medium-sized systems. For that purpose, the step-wise validation of various system properties (consistency, safety, progress) of the concurrent control software of a reactive system is performed. If possible, different analysis techniques are applied and compared with each other concerning its efforts.
Keywords: programmable logic controller; hierarchical place/transition nets; verification; temporal logics; model checking; interval nets.