Munta: A Verified Model Checker for Timed Automata | SpringerLink
Skip to main content
Springer Nature Link
Log in

Munta: A Verified Model Checker for Timed Automata

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11750))

Abstract

Munta is a mechanically verified model checker for timed automata, a popular formalism for modeling real-time systems. Our goal is two-fold: first, we want to provide a reference implementation that is fast enough to test other model checkers against it on reasonably sized benchmarks; second, the tool should be practical enough so that it can easily be used for experimentation. Munta can be compiled to Standard ML or OCaml and additionally features a web-based GUI. Its modeling language has a simple semantics but provides the most commonly used timed automata modeling features.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://wimmers.github.io/munta/.

  2. 2.

    https://reasonml.github.io/.

  3. 3.

    https://reasonml.github.io/reason-react/.

  4. 4.

    https://bucklescript.github.io/.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8

    Article  MathSciNet  MATH  Google Scholar 

  2. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_25

    Chapter  MATH  Google Scholar 

  3. Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_3

    Chapter  MATH  Google Scholar 

  4. Beyer, D., Lewerentz, C., Noack, A.: Rabbit: a tool for BDD-based verification of real-time systems. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 122–125. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_13

    Chapter  Google Scholar 

  5. Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_14

    Chapter  Google Scholar 

  6. Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12251-4_9

    Chapter  Google Scholar 

  7. Herbreteau, F., Point, G.: TChecker (2019). https://github.com/fredher/tchecker

  8. Hupel, L., Nipkow, T.: A verified compiler from Isabelle/HOL to CakeML. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 999–1026. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_35

    Chapter  Google Scholar 

  9. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  10. Lammich, P.: Generating verified LLVM from Isabelle/HOL. In: Proceedings of ITP 2019 (2019, to appear)

    Google Scholar 

  11. Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253–269. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_17

    Chapter  Google Scholar 

  12. Lammich, P.: Parser combinator library for Isabelle/HOL (2018). https://bitbucket.org/MohammadAbdulaziz/planning/src/master/isabelle/Parser_Combinator.thy

  13. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  14. Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A., Owens, S., Norrish, M.: A new verified compiler backend for CakeML. In: International Conference on Functional Programming (ICFP), pp. 60–73. ACM Press, September 2016. https://doi.org/10.1145/2951913.2951924, invited to special issue of Journal of Functional Programming

  15. Wang, F.: Efficient verification of timed automata with BDD-like datastructures. Int. J. Softw. Tools Technol. Transf. 6(1), 77–97 (2004). https://doi.org/10.1007/s10009-003-0135-4

    Article  Google Scholar 

  16. Wimmer, S.: Formalized timed automata. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 425–440. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_26

    Chapter  Google Scholar 

  17. Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 61–78. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_4

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität München, Munich, Germany

    Simon Wimmer

Authors
  1. Simon Wimmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Simon Wimmer .

Editor information

Editors and Affiliations

  1. Université Paris 13, Villetaneuse, France

    Étienne André

  2. University of Twente, Enschede, The Netherlands

    Mariëlle Stoelinga

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Wimmer, S. (2019). Munta: A Verified Model Checker for Timed Automata. In: André, É., Stoelinga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2019. Lecture Notes in Computer Science(), vol 11750. Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29662-9_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29661-2

  • Online ISBN: 978-3-030-29662-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation