Geodesic
A control flow graph based approach to make the~verification of cyber-physical systems using~KeYmaera easier
Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 5, pp. 465-480.

Voir la notice de l'article provenant de la source Math-Net.Ru

KeYmaera is an interactive theorem prover and is used to verify safety properties of cyber-physical systems (CPSs). It implements a Dynamic Logic for Hybrid Programs (HPs), while a HP models a CPS very precisely. Verifying properties of a given system in KeYmaera can become a challenge for a user since the proof is authored in a classical sequent calculus framework and a successful proof requires from the user intimate knowledge of the available calculus rules. Another barrier for widespread application of KeYmaera is the purely textual representation of current proof goals, what requires from the user very good training, experience, and patience. In this paper, we present an alternative verification approach based on KeYmaera, which drastically improves usability and minimizes user interaction. The main idea is to let the user annotate invariants and contracts to states of the hybrid automaton. Thus, the user can employ the graphical representation of the modelled system and is not bound to the purely textual form of hybrid programs as in KeYmaera. Based on the user-provided contracts, one can generate proof obligations, which are much simpler than the original proof goal in KeYmaera. The article is published in the authors' wording.
Keywords: CPS, KeYmaera, proof contracts, verification, hybrid systems, usability, interactive provers. 
@article{MAIS_2018_25_5_a1,
     author = {T. Baar and S. Staroletov},
     title = {A control flow graph based approach to make the~verification of cyber-physical systems {using~KeYmaera} easier},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {465--480},
     publisher = {mathdoc},
     volume = {25},
     number = {5},
     year = {2018},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a1/}
}
TY  - JOUR
AU  - T. Baar
AU  - S. Staroletov
TI  - A control flow graph based approach to make the~verification of cyber-physical systems using~KeYmaera easier
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2018
SP  - 465
EP  - 480
VL  - 25
IS  - 5
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a1/
LA  - en
ID  - MAIS_2018_25_5_a1
ER  - 
%0 Journal Article
%A T. Baar
%A S. Staroletov
%T A control flow graph based approach to make the~verification of cyber-physical systems using~KeYmaera easier
%J Modelirovanie i analiz informacionnyh sistem
%D 2018
%P 465-480
%V 25
%N 5
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a1/
%G en
%F MAIS_2018_25_5_a1
T. Baar; S. Staroletov. A control flow graph based approach to make the~verification of cyber-physical systems using~KeYmaera easier. Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 5, pp. 465-480. http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a1/

[1] Baudin P. et al., ACSL: ANSI/ISO C Specification Language. Version 1.12, https://frama-c.com/download/acsl_1.12.pdf

[2] Spin: Promela reference. float–floating point numbers, http://spinroot.com/spin/Man/float.html

[3] Alur R. et al., “Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems”, Hybrid Systems, Lecture Notes in Computer Science, 736, 1993, 209–229 | DOI | MR

[4] Behrmann G. et al., “A tutorial on uppaal”, Formal methods for the design of real-time systems, Springer, 2004, 200–236 | DOI | Zbl

[5] Booch G. et al., The unified modeling language user guide — covers {UML} 2.0, Addison Wesley object technology series, Second Edition, Addison-Wesley, 2005

[6] David A. et al., “Uppaal SMC tutorial”, International Journal on Software Tools for Technology Transfer, 17:4 (2015), 397–415 | DOI

[7] Floyd R.W., “Assigning Meanings to Programs”, Proceedings of Symposium on Applied Mathematics, 19 (1967), 19–32 | DOI | MR | Zbl

[8] Robert L. Grossman et al. (ed.), Hybrid Systems, Lecture Notes in Computer Science, 736, 1993 | DOI | Zbl

[9] Henzinger Thomas A., “The Theory of Hybrid Automata”, Proceedings 11th Annual {IEEE} Symposium on Logic in Computer Science, 1996, 278–292 | DOI | MR

[10] Kirchner F. et al., “Frama-C: A software analysis perspective”, Formal Aspects of Computing, 27:3 (2015), 573–609 | DOI | MR

[11] Nuzzo P. et al., “A platform-based design methodology with contracts and related tools for the design of cyber-physical systems”, Proceedings of the IEEE, 103:11 (2015), 2104–2132 | DOI

[12] Platzer A., Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, Heidelberg, 2010 | MR | Zbl

[13] Platzer A., “Logic and Compositional Verification of Hybrid Systems (Invited Tutorial)”, 23rd International Conference on Computer Aided Verification, Lecture Notes in Computer Science, 6806, 2011, 28–43 | DOI | MR

[14] Quesel J.-D. et al., “How to Model and Prove Hybrid Systemswith {KeYmaera}:A Tutorial on Safety”, STTT, 18:1 (2016), 67-91 | DOI

[15] Rümmer Ph., Princess Homepage, http://www.philipp.ruemmer.org/princess.shtml