KeYmaera User Tutorial: How to Model and Prove Hybrid Systems with KeYmaera

Table of Contents KeYmaera User Tutorial Abstract Selected Publications	KeYmaera or Source

KeYmaera User Tutorial

 

• How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety
• Tutorial examples: start KeYmaera and choose File->Load Project in its menu and select the project KeYmaera Tutorial
• Video tutorials

Abstract

This paper is a tutorial [8] on how to model and prove complex properties of complex hybrid systems in KeYmaera [4], an automatic and interactive formal verification tool for hybrid systems implementing differential dynamic logic [1,2]. Hybrid systems can model highly nontrivial controllers of physical plants, whose behaviors are often safety critical such as trains, cars, airplanes, or medical devices. Formal methods can help design systems that work correctly. This paper illustrates how KeYmaera can be used to systematically model, validate, and verify hybrid systems. We develop tutorial examples that illustrate challenges arising in many real-world systems. In the context of this tutorial, we identify the impact that modeling decisions have on the suitability of the model for verification purposes. We show how the interactive features of KeYmaera can help users understand their system designs better and prove complex properties for which the automatic prover of KeYmaera still takes an impractical amount of time. We hope this paper is a helpful resource for designers of embedded and cyber-physical systems and that it illustrates how to master common practical challenges in hybrid systems verification.

Keywords: formal verification of hybrid systems, differential dynamic logic, automated theorem proving, introduction to hybrid system modeling and verification

Selected Publications

The canonical references on the KeYmaera approach are [2] and [3]. The most comprehensive description of the KeYmaera approach can be found in the book [6]. Also see the publication reading guide.

1. Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer.
   How to model and prove hybrid systems with KeYmaera: A tutorial on safety.
   STTT 18(1), pp. 67-91, 2016. © The authors
   [bib | ⧉ | pdf | doi | mypdf | abstract]
   
   
2. André Platzer.
   Logics of dynamical systems.
   ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 13-24. IEEE 2012. © IEEE
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | abstract]
   
   
3. André Platzer.
   Logical Analysis of Hybrid Systems:
      Proving Theorems for Complex Dynamics.
   Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7.
   [bib | ⧉ | doi | book | web | errata | abstract]
   
   
4. André Platzer.
   Differential Dynamic Logics:
      Automated Theorem Proving for Hybrid Systems.
   PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
   ACM Doctoral Dissertation Honorable Mention Award in 2009.
   Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
   [bib | ⧉ | pdf | eprint | slides | book | ebook | abstract]
   
   
5. André Platzer and Jan-David Quesel.
   KeYmaera: A hybrid theorem prover for hybrid systems.
   In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pp. 171-178. Springer, 2008. © Springer
   [bib | ⧉ | pdf | doi | slides | tool | abstract]
   
   
6. André Platzer.
   Differential-algebraic dynamic logic for differential-algebraic programs.
   Journal of Logic and Computation 20(1), pp. 309-352, 2010.
   Special issue for selected papers from TABLEAUX'07. © The author
   [bib | ⧉ | pdf | doi | eprint | study | errata | TABLEAUX'07 | abstract]
   
   
7. André Platzer.
   Differential dynamic logic for hybrid systems.
   Journal of Automated Reasoning 41(2), pp. 143-189, 2008. © The author
   [bib | ⧉ | pdf | doi | mypdf | study | abstract]
   
   
8. André Platzer.
   Differential dynamic logic for verifying parametric hybrid systems.
   In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pp. 216-232. Springer, 2007. © Springer
   TABLEAUX Best Paper Award.
   [bib | ⧉ | pdf | doi | slides | study | TR | abstract]