COMBINED SYNTHESIS/VERIFICATION APPROACH TO PROGRAMMABLE LOGIC CONTROL OF A PRODUCTION

Abstract: The paper presents a methodology of designing control logic that is imple-mented by industrial programmable logic controllers. A two stage approach is proposed. In the rst stage a set of interlock supervisors is designed based on discrete-event model of the plant and a set of interlock specication models. Supervisory control theory is used to test the controllability of the specications and to derive a nite automaton representation of the admissible behaviour of the system. In the second stage the model of admissible behaviour is adopted as a plant model and used for the verication of the sequential specication model 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 an extension of Place/Transition nets is used, which includes external inputs and outputs, i.e., the Real-time Petri nets (RTPN). 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 sequential controller. Copyright '2005 IFA