A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier
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 si...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2018-10-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/752 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849240978324455424 |
|---|---|
| author | Thomas Baar Sergey Staroletov |
| author_facet | Thomas Baar Sergey Staroletov |
| author_sort | Thomas Baar |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-acb1df56afb74dc49f616ef6cd1c1b64 |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2018-10-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-acb1df56afb74dc49f616ef6cd1c1b642025-08-20T04:00:19ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172018-10-0125546548010.18255/1818-1015-2018-5-465-480525A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera EasierThomas Baar0Sergey Staroletov1Hochschule für Technik und Wirtschaft Berlin University of Applied SciencesPolzunov Altai State Technical UniversityKeYmaera 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.https://www.mais-journal.ru/jour/article/view/752cpskeymaeraproof contractsverificationhybrid systemsusabilityinteractive provers |
| spellingShingle | Thomas Baar Sergey Staroletov A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier Моделирование и анализ информационных систем cps keymaera proof contracts verification hybrid systems usability interactive provers |
| title | A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier |
| title_full | A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier |
| title_fullStr | A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier |
| title_full_unstemmed | A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier |
| title_short | A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier |
| title_sort | control flow graph based approach to make the verification of cyber physical systems using keymaera easier |
| topic | cps keymaera proof contracts verification hybrid systems usability interactive provers |
| url | https://www.mais-journal.ru/jour/article/view/752 |
| work_keys_str_mv | AT thomasbaar acontrolflowgraphbasedapproachtomaketheverificationofcyberphysicalsystemsusingkeymaeraeasier AT sergeystaroletov acontrolflowgraphbasedapproachtomaketheverificationofcyberphysicalsystemsusingkeymaeraeasier AT thomasbaar controlflowgraphbasedapproachtomaketheverificationofcyberphysicalsystemsusingkeymaeraeasier AT sergeystaroletov controlflowgraphbasedapproachtomaketheverificationofcyberphysicalsystemsusingkeymaeraeasier |