From HUPPAAL to UPPAAL - A Translation from Hierarchical Timed Automata to Flat Timed Automata

  • Alexandre David
  • M. Oliver Möller

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.

Published
2001-03-11
How to Cite
David, A., & Möller, M. O. (2001). From HUPPAAL to UPPAAL - A Translation from Hierarchical Timed Automata to Flat Timed Automata. BRICS Report Series, 8(11). https://doi.org/10.7146/brics.v8i11.20467