From HUPPAAL to UPPAAL: A Translation from Hierarchical
Timed Automata to Flat Timed Automata
Alexandre David
March 2001 |
Abstract:
We present a hierarchical version of timed automata, equipped
with data types, hand-shake synchronization, and local variables. We describe
the formal semantics of this hierarchical timed automata (HTA)
formalism in terms of a transition system.
We report on the implementation of a flattening algorithm, that translates our formalism to a network of UPPAAL timed automata. We establish a correspondence between symbolic states of an HTA and its translations, and thus are able to make use of UPPAAL's simulator and model checking engine. This technique is exemplified with a cardiac pacemaker model. Here, the overhead introduced by the translation is tolerable. We give run-time data for deadlock checking, timed reachability, and timed response analysis Available as PostScript, PDF. |