Extending a synthesis-centric model-based systems engineering framework with stochastic model checking

J. Markovski, E.S. Estens Musa, M.A. Reniers

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


    We propose to integrate performance evaluation with supervisory control synthesis to bring higher condence 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 xed piping in order to ensure greater exibility 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.
    Original languageEnglish
    Title of host publicationProceedings of the Sixth International Workshop on Practical Applications of Stochastic Modelling (PASM 2012), 17 September 2012, London, United Kingdom
    Place of PublicationAmsterdam
    Publication statusPublished - 2012
    Eventconference; PASM 2012 -
    Duration: 1 Jan 2012 → …

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    ISSN (Print)1571-0061


    Conferenceconference; PASM 2012
    Period1/01/12 → …
    OtherPASM 2012


    Dive into the research topics of 'Extending a synthesis-centric model-based systems engineering framework with stochastic model checking'. Together they form a unique fingerprint.

    Cite this