In: Proceedings of the IFAC-Safeprocess 2003, Washington (USA), pages 115-120. June 2003.
Abstract: Formal modeling and verification of a control algorithm allow to derive a correct and fault tolerant controller. In this contribution the combination of Signal Interpreted Petri Nets (SIPN) as formal model and symbolic model checking as verification method is proposed. To apply model checking, the SIPN is translated into a form accepted by the model checker and the properties to be verified are specified in temporal logic. A method for the automation of these tasks is presented. The algorithm generates an SMV input file containing a description of the SIPN and temporal logic formulae for standard properties of the controller.