Sciweavers

Share
STTT
2016

How to model and prove hybrid systems with KeYmaera: a tutorial on safety

4 years 3 months ago
How to model and prove hybrid systems with KeYmaera: a tutorial on safety
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 au...
Jan-David Quesel, Stefan Mitsch, Sarah M. Loos, Ni
Added 10 Apr 2016
Updated 10 Apr 2016
Type Journal
Year 2016
Where STTT
Authors Jan-David Quesel, Stefan Mitsch, Sarah M. Loos, Nikos Arechiga, André Platzer
Comments (0)
books