Verification of logic control design using SIPN and model checking - Methods and case study

This paper deals with the verification of logic control system designs by Signal Interpreted Petri Net (SIPN), which is a special extension of an ordinary petri net (PN) by input and output signals. Such extensions provide more power for a specification. However due to the extensions the basic petri net analysis method is not strong enough to determine the properties. The usual way to verify the correctness of the dynamic behavior is to employ a process model, which proves to be impractical in application, because the process model is usually not available. As a result requirement specifications given by users are difficult to be checked in this way. To solve this problem, a model checking approach has been applied to the verification of an SIPN design. The requirements to be verified are expressed in temporal logic (TL). Via a model checking algorithm the validity of such requirements can be checked automatically in every possible input sequences. In an error case a sequence of states is calculated, which indicates a trace leading to the violation of the requirements. A case study has shown that this approach can effectively locate errors in the design process.