A Flattening Algorithm for Hierarchical Timed Automata
- 15 Downloads
We propose a coherent algorithm for the translation of hierarchical timed automata into networks of (planar) timed automata. This kind of translation is called flattening. The two types of timed automata are used in formal verification of real-time systems: systems of parallel interacting components whose execution essentially depends not only on the order of the events in the system, but also on the real time of these events. The concept of hierarchical timed automaton covers the syntactic variations that are used in existing studies and are non-comparable by their expressive power. The number of states in a flattened network of time automata is of the least order among the flattening results of existing studies.
Keywordstimed automata formal verification real-time systems translation
Unable to display preview. Download preview PDF.
- 1.G. Behrmann, A. David, and K. G. Larsen, “A tutorial on Uppaal,” Formal methods in the design of real-time systems, in: 4th Int. School of Formal Methods for the Design of Computer, Communication, and Software Systems, 3185, SFM-RT 2004, LNCS (2004), pp. 200–236.Google Scholar
- 2.A. David, M. O. Moeller, and W. Yi, “Formal verification of UML statecharts with real-time extensions,” Fund. Appr. to Software Eng., 218–232 (2002).Google Scholar
- 3.C. Baker and J.-P. Katoen, Principles of Model Checking, MIT Press (2008).Google Scholar
- 4.A. David and M. O. Moller, “From HUppaal to Uppaal: A translation from hierarchical times automata to flat timed automata,” Research Series RS-01-11, BRICS, Dept. Computer Sci., Univ. Aarhus (March 2001).Google Scholar
- 6.D. Yu. Volkanov, V. A. Zakharov, D. A. Zorin, V. V. Podymov, and I. V. Konnov, “A combined toolset for the verification of real-time distributed systems,” Programm., No. 6, 73–82 (2015).Google Scholar