How to model and prove hybrid systems with KeYmaera: a tutorial on safety
Open Access
- 27 February 2015
- journal article
- Published by Springer Science and Business Media LLC in International Journal on Software Tools for Technology Transfer
- Vol. 18 (1), 67-91
- https://doi.org/10.1007/s10009-015-0367-0
Abstract
This paper is a tutorial on how to model hybrid systems as hybrid programs in differential dynamic logic and how to prove complex properties about these complex hybrid systems in KeYmaera, an automatic and interactive formal verification tool for hybrid systems. 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
This publication has 53 references indexed in Scilit:
- Exact and fully symbolic verification of linear hybrid automata with large discrete state spacesScience of Computer Programming, 2012
- Differential-algebraic Dynamic Logic for Differential-algebraic ProgramsJournal of Logic and Computation, 2008
- PHAVer: algorithmic verification of hybrid systems past HyTechInternational Journal on Software Tools for Technology Transfer, 2008
- Safety verification of hybrid systems by constraint propagation-based abstraction refinementACM Transactions on Embedded Computing Systems, 2007
- QEPCAD BACM SIGSAM Bulletin, 2003
- Conflict resolution for air traffic management: a study in multiagent hybrid systemsIEEE Transactions on Automatic Control, 1998
- HYTECH: a model checker for hybrid systemsInternational Journal on Software Tools for Technology Transfer, 1997
- REDLOGACM SIGSAM Bulletin, 1997
- SHIFT: A formalism and a programming language for dynamic networks of hybrid automataLecture Notes in Computer Science, 1997
- The algorithmic analysis of hybrid systemsTheoretical Computer Science, 1995