An integrated state- and event-based framework for verifying liveness in supervised systems

Supervisory control theory deals with synthesis of discrete-event supervisory controllers that ensure safe (and nonblocking) behavior of the supervised system. However, the synthesized supervisor comes with no guarantees regarding desired functionality beyond nonblocking behavior. This typically occurs when the control requirements imposed on the system are too strict, or the model of the system needs to be refined. To provide concise and useful feedback to the modeler, we propose an integrated state- and event-based systems engineering framework using state-of-the-art tools: Supremica for supervisor synthesis and mCRL2 for verification. Stating properties in terms of both states and transitions is important in the domain of supervisor synthesis as many control and liveness requirements involve combined state- and event-based specifications. However, many of the available verification tools either focus on state-based or event-based properties. We seek to remedy this situation by providing verification patterns that typically occur in industrial application of supervisory control. We illustrate the framework by revisiting an industrial case study of coordinating maintenance procedures of a high-tech Oce printer, for which we verify the functionality of the solution.