Klein, S; Frey, G; Minas, M:
PLC Programming with Signal Interpreted Petri Nets.
Proceedings of the ICATPN 2003, Eindhoven (The Netherlands), LNCS 2679, pp. 440-449, Springer Verlag, June 2003.

    In this paper a graphical editor to design Programmable Logic Controller (PLC) programs using Signal Interpreted Petri Nets (SIPN) is presented. SIPN are an extension of condition event Petri nets that allow the handling of input and output signals. The presented tool, SIPN Editor, has been developed using DiaGen which is an environment for rapidly developing diagram editors from a formal specification of the diagram language. The SIPN Editor supports the translation of SIPN into input code for the model checker SMV. Using SMV, the SIPN can be verified before it is automatically translated into Instruction List code according to the IEC 61131-3 standard. This code can be downloaded on nearly every PLC.