Extending a Synthesis-Centric Model-Based Systems Engineering Framework with Stochastic Model Checking

We propose to integrate performance evaluation with supervisory control synthesis to bring higher confidence in the control design. Supervisory control theory deals with automatic synthesis of supervisory controllers that ensure safe behavior of the supervised system, based on the models of the uncontrolled system and the (safety) control requirements. For the purpose of performance evaluation, we turn to stochastic model checking of continuous-time Markov chains, which requires an extension of the model of the uncontrolled system with Markovian delays. We cast our proposal as an extension of a model-based systems engineering framework that relies on supervisor synthesis. We treat the Markovian delays syntactically, exploiting their equivalent interleaving behavior with uniquely-named uncontrollable transitions. In this way, we can employ already available synthesis tools, while preserving the stochastic behavior. To this end, we develop model transformation tools to extract the underlying Markov process from the stochastic discrete-event model of the supervised system. We illustrate the approach by modeling a pipeless plant that employs automated guided vehicles instead of fixed piping in order to ensure greater flexibility of the plant. The control problem that we solve is safe high-level movement coordination of the vehicles, ensured by the supervisory controller. We show how to seamlessly introduce stochastic behavior in the supervised system and we evaluate several performance and reliability aspects of the plant. We implement the framework by interfacing two state-of-the-art tools: Supremica for supervisory controller synthesis and MRMC for Markovian model checking. To this end, we improve previous attempts by providing support for data-based observers, which greatly improve the modeling capabilities of the framework.