DocumentCode :
645993
Title :
An integrated systems engineering framework for supervisor synthesis, verification, and performance evaluation
Author :
Markovski, Jasen
Author_Institution :
Dept. of Mech. Eng., Eindhoven Univ. of Technol., Eindhoven, Netherlands
fYear :
2013
fDate :
17-19 July 2013
Firstpage :
650
Lastpage :
657
Abstract :
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.
Keywords :
Markov processes; computational complexity; control system CAD; control system synthesis; discrete event systems; formal verification; stochastic systems; systems engineering; MRMC; Markov reward model checker; Supremica; UPPAAL; computational complexity; coordinating printing maintenance procedures; discrete-event models; functional properties; integrated systems engineering framework; labeled interactive Markov chain; model-based systems engineering framework; performance evaluation; post-synthesis validation; quantitative properties; quantitative supervised behavior; stochastic behavior; stochastic model checker; stochastic nondeterministic discrete-event systems; supervisor synthesis; supervisor verification; supervisory control theory; supervisory controllers; Automata; Maintenance engineering; Modeling; Printing; Software; Stochastic processes; Supervisory control;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Control Conference (ECC), 2013 European
Conference_Location :
Zurich
Type :
conf
Filename :
6669190
Link To Document :
بازگشت