A process-theoretic state-based framework for live supervision

We propose a model-based systems engineering framework that couples supervisory control and verification. The framework has a process-theoretic backbone, which supports all required concepts, and it is implemented using state-of-the-art tools: Supremica for supervisor synthesis and UPPAAL for state-based verification. The process theory relies on partial bisimulation to model controllability and propositional signal emission to model a supervisory control loop with state-based observations. Supremica can model the signal observation by employing finite integer variables and action guards, whereas the supervised system can be consistently translated to UPPAAL by using a translation tool we developed. We illustrate the framework by revisiting an industrial case study of coordinating maintenance procedures of a high-tech Océ printer.