|
Linear Parametric Model Checking of Timed Automata
Thomas S. Hune
January 2001 |
Abstract:
We present an extension of the model checker UPPAAL
capable of synthesize linear parameter constraints for the correctness of
parametric timed automata. The symbolic representation of the (parametric)
state-space is shown to be correct. A second contribution of this paper is
the identification of a subclass of parametric timed automata (L/U automata),
for which the emptiness problem is decidable, contrary to the full class
where it is know to be undecidable. Also we present a number of lemmas
enabling the verification effort to be reduced for L/U automata in some
cases. We illustrate our approach by deriving linear parameter constraints
for a number of well-known case studies from the literature (exhibiting a
flaw in a published paper)
Available as PostScript, PDF. |