The KeYmaera X Theorem Prover: Hybrid Systems Verification and Verified Runtime Validation
Presented as part of the 2018 HCSS conference.
BIO
Stefan Mitsch is a System Scientist in the Logical Systems Lab of Carnegie Mellon's Computer Science Department. He received his PhD in computer science from Johannes Kepler University in 2012. His research focuses on modeling, formal verification, and verified runtime safety methods for cyber-physical systems. He is particularly interested in applying software engineering methods to support system design and verification.
ABSTRACT
Formal verification plays a crucial role in making cyber-physical systems safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained. Models including both controller and physical dynamics are essential; but any model we could possibly build, no matter how detailed, necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified with respect to the model. Otherwise, all bets are off. For true safety, we need to combine formal verification of models with methods to ensure that these verification results obtained offline provably apply to implementations at runtime.
Formal Verification in KeYmaera X. KeYmaera X [1] is a theorem prover for hybrid systems, i. e., systems with interacting discrete and continuous dynamics, which arise in virtually all mathematical models of cyber-physical systems.1 It implements differential dynamic logic (dL [2,3,4]) for hybrid programs, a program notation for hybrid systems. It also provides the necessary foundations for adversarial settings using hybrid games [5]. KeYmaera X was used in several case studies, e.g., for analyzing safety of vertical collision avoidance maneuvers in the next-generation airborne collision avoidance protocol ACAS X [6] and for ground robot collision avoidance [7].
Verification support in KeYmaera X for complex heterogeneous systems features a small-kernel architecture [1] to increase trust in proofs, tactical theorem proving [8] to automate new proofs, adapt existing proofs, and compose proofs about sub-systems to system proofs [9,10].
Verified Runtime Validation in KeYmaera X. Runtime verification and validation methods are lightweight formal methods that monitor a system for violation of properties during the system’s normal operation. With our verified runtime validation method ModelPlex [11,12], implemented in KeYmaera X, we use theorem proving to approach runtime monitoring from a complementary perspective: what are the right properties to monitor in order to ensure safety? Due to the inevitability of modeling challenges in CPS, this makes ModelPlex, so far, the only technique that can transfer offline guarantees about CPS models to online guarantees about the running CPS.
ModelPlex can help increase trust in autonomy by sandboxing unverified implementations and by monitoring for unexpected behavior in the environment. For example, ModelPlex-generated monitors provided a basis for addressing the safety of reinforcement learning [13]. The underlying idea of ModelPlex is that correct monitoring properties must detect non-compliance between a model and reality based on sensor measurements. Compliance amounts to comparing observations at different times with the predictions of a model. Instead of running models, which can be computationally expensive due to differential equations, a major insight of ModelPlex is that much of the expensive computation can be done offline with a formal proof, resulting in purely arithmetical conditions on the relationship between sensor values, control output, and their history. These conditions, if shown to be true at system runtime from verifiably correct implementations [14], provably witness compliance between the model and reality. The resulting monitor and the observed system execution are, thus, accompanied by a correctness proof.
References:
1. Fulton, N., Mitsch, S., Quesel, J.D., Volp, M., Platzer, A.: KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Felty, A.P., ¨Middeldorp, A., eds.: CADE. Volume 9195 of LNCS., Springer (2015) 527–538
2. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2) (2008) 143–189
3. Platzer, A.: Logics of dynamical systems. In: LICS, IEEE (2012) 13–24
4. Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. (2016)
5. Platzer, A.: Differential game logic. ACM Trans. Comput. Log. 17(1) (2015) 1:1–1:51
6. Jeannin, J., Ghorbal, K., Kouskoulas, Y., Schmidt, A., Gardner, R., Mitsch, S., Platzer, A.: A formally verified hybrid system for safe advisories inthe next-generation airborne collision avoidance system. STTT (2016)
7. Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. I. J. RoboticsRes. 36(12) (2017) 1312–1340
8. Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: Tactical theorem proving for hybrid systems. In Ayala-Rincon, M., Mu ´ noz, C.A., eds.: ˜ITP. Volume 10499 of LNCS., Springer (2017) 207–224
9. Muller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: A component-based approach to hybrid systems safety verification. In ¨Abraham, E., Huisman, M., eds.: IFM. Volume 9681 of LNCS., Springer (2016) 441–456
10. Muller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: Change and delay contracts for hybrid system component verification. In ¨Huisman, M., Rubin, J., eds.: FASE. Volume 10202 of LNCS., Springer (2017) 134–151
11. Mitsch, S., Platzer, A.: ModelPlex: Verified runtime validation of verified cyber-physical system models. In Bonakdarpour, B., Smolka, S.A., eds.:RV. Volume 8734 of LNCS., Springer (2014) 199–214
12. Mitsch, S., Platzer, A.: ModelPlex: Verified runtime validation of verified cyber-physical system models. Form. Methods Syst. Des. 49(1) (2016)33–74 Special issue of selected papers from RV’14.
13. Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: Toward safe control through proof and learning. In McIlraith, S.,Weinberger, K., eds.: Proceedings of the 32nd AAAI Conference, February 2-7, 2018, New Orleans, Louisiana, USA, AAAI Press (2018)
14. Bohrer, B., Tan, Y.K., Mitsch, S., Myreen, M., Platzer, A.: VeriPhy: Verified controller executables from verified cyber-physical system models.
(2018) (conditionally accepted at PLDI).
--------
1 KeYmaera X is available at http://keymaeraX