SK_GF_LL_IFACSAFE2003_june_2003

Klein, S.; Frey, G.; Litz, L.:
Designing fault-tolerant Controllers using SIPN and Model-Checking.
Proceedings of the IFAC-Safeprocess 2003, Washington (USA), pp. 115-120, June 2003.

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.