A flattening algorithm for hierarchical timed automata.

*(English. Russian original)*Zbl 1423.68265
Comput. Math. Model. 30, No. 2, 99-106 (2019); translation from Prikl. Mat. Inf. 59, 5-15 (2018).

Summary: 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.

##### MSC:

68Q45 | Formal languages and automata |

68Q60 | Specification and verification (program logics, model checking, etc.) |

##### Software:

Uppaal
PDF
BibTeX
XML
Cite

\textit{V. V. Podymov}, Comput. Math. Model. 30, No. 2, 99--106 (2019; Zbl 1423.68265); translation from Prikl. Mat. Inf. 59, 5--15 (2018)

Full Text:
DOI

##### References:

[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. · Zbl 1105.68350 |

[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). · Zbl 1059.68542 |

[3] | C. Baker and J.-P. Katoen, Principles of Model Checking, MIT Press (2008). |

[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). |

[5] | Volkanov, DY; Zakharov, VA; Zorin, DA; Konnov, IV; Podymov, VV, How to develop a simple verification tool for real-time systems, Model. i Anal. Inform. Sist., 19, 45-56, (2012) |

[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). |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.