Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
An Isabelle/HOL Formalisation of Green’s Theorem Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Formalized Timed Automata

Author : Simon Wimmer

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Modular Dependent Induction in Coq, Mendler-Style
next chapter AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
Footnotes
1
We assume a default clock numbering, mapping https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_26/419043_1_En_26_IEq43_HTML.gif to index https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_26/419043_1_En_26_IEq44_HTML.gif , for our examples.
 
2
https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_26/419043_1_En_26_IEq56_HTML.gif denotes the empty list and \(x \cdot xs\) is a list constructed from head x and tail xs.
 
3
https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_26/419043_1_En_26_IEq60_HTML.gif is the set of elements contained in https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_26/419043_1_En_26_IEq61_HTML.gif .
 
4
https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_26/419043_1_En_26_IEq141_HTML.gif denotes the fractional part of any real number https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_26/419043_1_En_26_IEq142_HTML.gif .
 
Literature
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)CrossRef
2.
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)
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)CrossRef
5.
Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003)
6.
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)CrossRef
8.
9.
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)CrossRef
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)CrossRef
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)CrossRef
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)MATH
13.
Larsen, G.K., Pettersson, P., Yi, W.: Uppaal in a nutshell. Softw. Tools Technol. Transf. 1(1), 134–152 (1997)CrossRefMATH
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)CrossRef
15.
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)
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)CrossRefMATH
Metadata
Title
Formalized Timed Automata
Author
Simon Wimmer
Copyright Year
2016
Book
Interactive Theorem Proving

Print ISBN: 978-3-319-43143-7

Electronic ISBN: 978-3-319-43144-4

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-43144-4_26

Premium Partner

    Image Credits