TY - GEN
T1 - Extending a synthesis-centric model-based systems engineering framework with stochastic model checking
AU - Markovski, J.
AU - Estens Musa, E.S.
AU - Reniers, M.A.
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
M3 - Conference contribution
T3 - Electronic Notes in Theoretical Computer Science
SP - 1
EP - 15
BT - Proceedings of the Sixth International Workshop on Practical Applications of Stochastic Modelling (PASM 2012), 17 September 2012, London, United Kingdom
PB - Elsevier
CY - Amsterdam
T2 - conference; PASM 2012
Y2 - 1 January 2012
ER -