Abstract
Timed automata are a widely used formalism for modeling real-time systems, which is employed in a class of successful model checkers such as UPPAAL. These tools can be understood as trust-multipliers: we trust their correctness to deduce trust in the safety of systems checked by these tools. However, mistakes have previously been made. This particularly regards an approximation operation, which is used by model-checking algorithms to obtain a finite search space. The use of this operation left a soundness problem in the tools employing it, which was only discovered years after the first model checkers were devised. This work aims to provide certainty to our knowledge of the basic theory via formalization in Isabelle/HOL: we define the main concepts, formalize the classic decidability result for the language emptiness problem, prove correctness of the basic forward analysis operations, and finally outline how both streams of work can be combined to show that forward analysis with the common approximation operation correctly decides emptiness for the class of diagonal-free timed automata.
Supported by DFG project NI 491/16-1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We assume a default clock numbering, mapping
to index
, for our examples.
- 2.
denotes the empty list and \(x \cdot xs\) is a list constructed from head x and tail xs.
- 3.
is the set of elements contained in
.
- 4.
denotes the fractional part of any real number
.
References
Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, pp. 592–601 (1993)
Bengtsson, J.E., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003)
Bouyer, P.: Forward analysis of updatable timed automata. Form. Methods Syst. Des. 24(3), 281–320 (2004)
Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Are timed automata updatable? In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 464–479. Springer, Heidelberg (2000)
Castéran, P., Rouillard, D.: Towards a generic tool for reasoning about labeled transition systems. In: TPHOLs 2001: Supplemental Proceedings (2001). http://www.informatics.ed.ac.uk/publications/report/0046.html
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
Garnacho, M., Bodeveix, J.P., Filali-Amine, M.: A mechanized semantic framework for real-time systems. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 106–120. Springer, Heidelberg (2013)
Henzinger, T.A., Ho, P.-H., Wong-toi, H.: Hytech: a model checker for hybrid systems. Softw. Tools Technol. Transf. 1(1), 460–463 (1997)
Larsen, G.K., Pettersson, P., Yi, W.: Uppaal in a nutshell. Softw. Tools Technol. Transf. 1(1), 134–152 (1997)
Paulin-Mohring, C.: Modelisation of timed automata in Coq. In: Kobayashi, N., Babu, C.S. (eds.) TACS 2001. LNCS, vol. 2215, pp. 298–315. Springer, Heidelberg (2001)
Wimmer, S.: Timed automata. Archive of Formal Proofs, March 2016. http://isa-afp.org/entries/Timed_Automata.shtml, Formal proof development
Xu, Q., Miao, H.: Formal verification framework for safety of real-time system based on timed automata model in PVS. In: Proceedings of the IASTED International Conference on Software Engineering, pp. 107–112 (2006)
Xu, Q., Miao, H.: Manipulating clocks in timed automata using PVS. In: Proceedings of SNPD 2009, pp. 555–560 (2009)
Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Proceedings of Formal Description Techniques VII, pp. 243–258 (1994)
Yovine, S.: KRONOS: a verification tool for real-time systems. Softw. Tools Technol. Transf. 1(1), 123–133 (1997)
Acknowledgement
I would like to thank Tobias Nipkow and the anonymous reviewers for their helpful comments on earlier versions of this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Wimmer, S. (2016). Formalized Timed Automata. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_26
Download citation
DOI: https://doi.org/10.1007/978-3-319-43144-4_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-43143-7
Online ISBN: 978-3-319-43144-4
eBook Packages: Computer ScienceComputer Science (R0)