Affiliations: Dept. of Engineering Science, Martin-Luther-University, Halle-Wittenberg, Germany. email: hans-michael.hanisch@iw.uni-halle.de | Dept. of Electrical Engineering, Institute for Automation Technology (IFAT), Otto-von-Guericke-University, Magdeburg, Germany. email: arndt.lueder@e-technik.uni-magdeburg.de
Note: [] Address for correspondence: Dept. of Engineering Science, Martin-Luther-University, Halle-Wittenberg, Germany
Note: [] Address for correspondence: Dept. of Electrical Engineering, Institute for Automation Technology (IFAT), Otto-von-Guericke-University, Magdeburg, Germany
Abstract: Petri nets have a longstanding history in controller design and implementation, and it is often told that they have the dominating position in this field due to the close relationship between Petri nets and Graphcet or other sequential function diagrams. We want to show that there are some severe problems when Petri nets are used to describe both: the controller and the plant under control. The nature of these problems is the lack of a concept of input and output signals and, moreover, the lack of a formal concept to interconnect systems modeled by Petri nets via signals. Although this is often neglected, it turns out to be a key issue if a model of the closed-loop behavior must be established as a precondition for formal controller verification. We present a signal extension for Petri nets and means for interconnecting an arbitrary number of those extended Petri nets. We come up with the conclusion that the resulting models are suited for controller verification. Although the graphical appearance shows similarities to Petri nets, the resulting models are no longer Petri nets.
Keywords: Controller verification, Discrete event systems, Petri nets
