KS_XW_GF_JJL_LL_ACC2002_may_2002

Klein, S., Weng, X., Frey, G., Lesage, J.-J. and Litz, L.:
Controller Design for an FMS using Signal Interpreted Petri Nets and SFC.
roceedings of the American Control Conference 2002 (ACC2002), Anchorage, Alaska, pp. 4141-4146, May 2002.

The aim of this paper is to study 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 Sig-nal Interpreted Petri Nets, validated using Model-checking techniques and translated into a Sequential Function Charts (SFC) implementation program. This program is then vali-dated 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).