×

zbMATH — the first resource for mathematics

Formalized timed automata. (English) Zbl 06644758
Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-43143-7/pbk; 978-3-319-43144-4/ebook). Lecture Notes in Computer Science 9807, 425-440 (2016).
Summary: 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.
For the entire collection see [Zbl 1343.68004].
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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) · Zbl 0765.68150 · doi:10.1007/BFb0032042
[2] Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[3] 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) · Zbl 1310.68139 · doi:10.1145/167088.167242
[4] 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) · Zbl 1088.68119
[5] Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003) · doi:10.1007/3-540-36494-3_54
[6] Bouyer, P.: Forward analysis of updatable timed automata. Form. Methods Syst. Des. 24(3), 281–320 (2004) · Zbl 1073.68041 · doi:10.1023/B:FORM.0000026093.21513.31
[7] 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) · Zbl 0974.68084 · doi:10.1007/10722167_35
[8] 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
[9] Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001) · doi:10.1016/B978-044450813-3/50026-6
[10] 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) · doi:10.1007/3-540-52148-8_17
[11] 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) · Zbl 1390.68470 · doi:10.1007/978-3-642-40229-6_8
[12] 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) · Zbl 1060.68603
[13] Larsen, G.K., Pettersson, P., Yi, W.: Uppaal in a nutshell. Softw. Tools Technol. Transf. 1(1), 134–152 (1997) · Zbl 1060.68577 · doi:10.1007/s100090050010
[14] 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) · Zbl 1087.68575 · doi:10.1007/3-540-45500-0_15
[15] Wimmer, S.: Timed automata. Archive of Formal Proofs, March 2016. http://isa-afp.org/entries/Timed_Automata.shtml , Formal proof development
[16] 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)
[17] Xu, Q., Miao, H.: Manipulating clocks in timed automata using PVS. In: Proceedings of SNPD 2009, pp. 555–560 (2009) · doi:10.1109/SNPD.2009.69
[18] 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)
[19] Yovine, S.: KRONOS: a verification tool for real-time systems. Softw. Tools Technol. Transf. 1(1), 123–133 (1997) · Zbl 1060.68606 · doi:10.1007/s100090050009
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.