Linear Parametric Model Checking of Timed Automata

Abstract

We present an extension of the model checker Uppaal capable
of synthesizing 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).