In: Proceedings of CESA 2003, Lille (France), pages CD-Rom paper S2-I-04-0176. July 2003.
Abstract: In this paper the advantages of verification and validation to support changes of an existing PLC program are shown. The controller is defined using Signal Interpreted Petri Nets (SIPN) and verification and validation are performed using symbolic model-checking. The main focus of this paper is to show the process and the benefits of verification and validation for the reliability of the control algorithm when specified changes are to make. This is clarified by the example of a heating tank controller throughout the text.