Controller design for an FMS using Signal Interpreted Petri Nets and SFC: Validation of both descriptions via model-checking

This paper studies the validation of both the behavioral model and the implementation program of an automated system. To clarify our approach, we use a small production line whose control algorithm is built using signal interpreted Petri nets, validated using model-checking techniques and translated into a sequential function charts (SFC) implementation program. This program is then validated anew. Using this example, we show the utility of those two validation steps before the final implementation of the program on a programmable logic controller (PLC).