GF_JJL_SK_LL_CESA_jul_2003

Klein, S.; Frey, G.; Litz, L.; Lesage, J.-J.:
Supporting the Changeability of SIPN-based Logic Control Algorithms by Verification and Validation
Proceedings of CESA 2003, Lille (France), CD-Rom paper S2-I-04-0176, July 2003.

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.