An integrated systems engineering framework for supervisor synthesis, verification, and performance evaluation

We propose a model-based systems engineering framework that enables supervisor synthesis of stochastic (nondeterministic) discrete-event systems, and post-synthesis validation of functional and quantitative properties of the supervised system. Supervisory control theory deals with synthesis of models of supervisory controllers that ensure safe and nonblocking behavior, based on discrete-event models of the uncontrolled system and the control requirements. Typically, neither more elaborated functional properties nor performance metrics can be guaranteed by the synthesis procedure for large systems, due to high computational complexity. Thus, the supervised system must be validated to ensure that intended behavior is present. The framework employs a single integrated model that denotes all relevant aspects of the system. We rely on state-of-the-art tools to implement the proposed framework. For supervisor synthesis we employ Supremica, which models we extend to denote stochastic behavior. For verification, we provide a consistent translation of the supervised system to the model checker UPPAAL. To evaluate quantitative supervised behavior, first we transform the denoted system model to a labeled Interactive Markov chain and couple it with the synthesized supervisor. Then, we derive the underlying labeled Markov process and feed it to the stochastic model checker MRMC. We illustrate the framework on an industrial case study of coordinating printing maintenance procedures.