In: J.-M. Colom, M. Koutny (Eds.), Newcastle upon Tyne, UK: Proc. of 22nd International Conf. on Applications and Theory of Petri Nets 2001 (ICATPN 2001), pages 144-163. Lecture Notes in Computer Science 2075, edited by G. Goos, J. Hartmanis and J. van Leuwen, Springer, June 2001.
Abstract: We address the verification of programmable logic controllers (PLC). In our approach, a PLC program is translated into a special type of colored Petri net, a so-called register net (RN). We present analysis methods based on the partial order semantics of RN's, which allow the generation of partial order traces as counter examples in the presence of programming errors. To that purpose, the behavior description `concurrent automaton', introduced in [3] for safe Petri nets, is upliftet to the dedicated RN's.