A Graph-Based Transformation Reduction to Reach UPPAAL States Faster

Autor:	Dieter Gollmann, Jonas Rinast, Sibylle Schupp
Rok vydání:	2014
Předmět:	Model checking Computer science Graph based Graph (abstract data type) Abstraction model checking Algorithm
Zdroj:	Lecture Notes in Computer Science ISBN: 9783319064093 FM
DOI:	10.1007/978-3-319-06410-9_37
Popis:	On-line model checking is a recent technique to overcome limitations of model checking if accurate system models are not available. At certain times during on-line model checking it is necessary to adjust the current model state to the real-world state and to do so in an efficient way. This paper presents a general, graph-based transformation reduction and applies it to reduce the length of transformation sequences needed to reach particular states in the model checker UPPAAL. Our evaluation shows that, generally, for the length of those sequences upper bounds exist independently from the elapsed time in the system. It follows that our proposed method is capable of fulfilling the real-time requirements imposed by on-line model checking.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::39fe75fbbceab8e8e5ac2d4b07d53672 https://doi.org/10.1007/978-3-319-06410-9_37 Zobrazit plný text záznamu