In: Proc. 2nd Int. Workshop on Manufacturing and Petri Nets held at Int. Conf. on Application and Theory of Petri Nets (ICATPN '97), Toulouse, June 1997, pages 69-84. 1997. Available at http://www.informatik.tu-cottbus.de/~wwwdssz/publications/papers.html.
Abstract: The development of provably error-free and efficient concurrent manufacturing 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 demonstrates that available methods and tools are actually applicable successfully to at least medium-sized manufacturing systems. For that purpose, step-wise validation of various system properties (consistency, safety, progress) and optimization of the concurrent controller software of a discrete event system is performed. If possible, different analysis techniques are applied and compared with each other concerning their efforts.
Keywords: programmable logic controller; hierarchical place/transition nets; verification; optimization; temporal logics; model checking; interval nets.