Combined synthesis/verification approach to programmable logic control of a production line

A two stage methodology of designing control logic that is implemented by industrial programmable logic controllers is presented. A set of interlock supervisors is designed first based on discrete-event model of the plant and a set of interlock specification models. Supervisory control theory is used to derive a finite automaton representation of the admissible behaviour. In the second stage this model is adopted as a plant model and used for the verification of the sequential specification in a form of a Petri net. The basic property of interest is the absence of blocking. To study the interaction of the two models the Real-time Petri nets (RTPN) extension of Place/Transition nets is used. A new kind of reachability analysis is applied, which considers all possible changes of the controller input and output signals. This enables to verify the nonblocking operation of the controller.