Application of Model-Checking Technology to Controller Synthesis

Autor:	Jacob Illum Rasmussen, Alexandre David, Jacob Deleuran Grunnet, Jan Jakob Jessen, Kim Guldstrand Larsen
Rok vydání:	2011
Předmět:	Model checking Control theory Computer science Distributed computing Hybrid system Control (management) Linear matrix inequality Control engineering Domain (software engineering)
Zdroj:	Formal Methods for Components and Objects ISBN: 9783642252709 FMCO
DOI:	10.1007/978-3-642-25271-6_18
Popis:	In this paper we present two frameworks that have been implemented to link traditional model-checking techniques to the domain of control. The techniques are based on solving a timed game and using the resulting solution (a strategy) as a controller. The obtained discrete controller must fit within its continuous environment, which is modelled and taken care of in our frameworks. Our first technique does it by using Matlab to discretise the problem and then Uppaal-tiga to solve the obtained timed game. This is implemented as a toolbox. The second technique relies on the user defining a timed game model in Uppaal-tiga. Then the strategy is automatically imported in Simulink as an S-function for simulation and validation purposes. We demonstrate the effectiveness of these frameworks in different case-studies.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::edc879b462f5605cc1d81c93cf6906d1 https://doi.org/10.1007/978-3-642-25271-6_18 Zobrazit plný text záznamu