Advertisement
Published in:
2011 | OriginalPaper | Chapter
Robust Model-Checking of Timed Automata via Pumping in Channel Machines
Authors : Patricia Bouyer, Nicolas Markey, Ocan Sankur
Published in: Formal Modeling and Analysis of Timed Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satisfied by digital hardware on which the models are implemented. In fact, it was shown that the presence of imprecisions, however small they may be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system.
The problem of robust model-checking was then defined to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct.
In this work, we show that robust model-checking against
ω
-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of
ω
-regular properties, which is both optimal and valid for general timed automata.