PLC Programs Design Using Signal Interpreted Petri Networks

The paper presents an approach for designing dependable programmable logic controller (PLC) programs. It starts from informal specifications and ends with the final implementation on a real PLC. The approach uses Signal InterpretedPetri Networks (SIPNs) for modeling the control algorithm, model checking for model verification and validation, and automatic Instruction List (IL) program generation. Finally, the IL program is tested on a real PLC. A simple example is used throughout the paper in order to illustrate the framework. The advantage of the approach consists in the correctness of the resulting PLC programs, which makes them much more dependable than direct implemented PLC code.