@TechReport{BRICS-RS-01-11,
  author =       "David, Alexandre and M{\"o}ller, M. Oliver",
  title =        {{F}rom {{\sc HUppaal}} to {{\sc Uppaal}}: {A} translation from
		  hierarchical timed automata to flat timed automata},
  spinetitle =   {{F}rom {H}ierarichcal {T}imed {A}utomata to {\sc {U}ppaal}},
  institution =  "{BRICS}",
  year =         2001,
  type =         "Research Series",
  number =       "RS-01-11",
  address =       "Department of Computer Science, University of Aarhus",
  OPTkey =       "",
  month =        mar,
  OPTnote =      "",
  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 {\em hierarchical timed
                  automata} (HTA) formalism in terms of a transition
                  system.\bibpar We report on the implementation of a
                  flattening algorithm, that translates our formalism
                  to a network of {\sc Uppaal} timed automata. We
                  establish a correspondence between symbolic states
                  of an HTA and its translations, and thus are able to
                  make use of {\sc Uppaal}'s simulator and model
                  checking engine.\bibpar 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",
  OPTlinkhtmlabs ="",
  OPTlinkdvi =   "",
  OPTlinkps =    "",
  OPTlinkpdf =   "",
  OPTannote =    ""
}