Verification of process operations using model checking

In order to decrease time to market for products it is important to decrease the time for implementation and debugging of the control logic that are used to manufacture the products. In this paper, an approach based on a high-level specification of the relations between process operations and resources and the use of formal verification is presented. By using formal verification it is possible to find potential errors within the specification at an early stage in the development process. In this work it is shown how the high-level specifications may be translated into extended finite automata, and how these extended finite automata may be efficiently verified using the symbolic model checking tool, NuSMV. It is also shown how the presented approach is suitable for verification of general supervisory control properties like controllability and non-blocking.