In: Proceedings of the American Control Conference 2002 (ACC2002), Anchorage, Alaska, pages 4141-4146. May 2002.
Abstract: 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).