A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier

Modelirovanie i Analiz Informacionnyh Sistem

Thomas Baar¹  Sergey Staroletov² 

[1] Hochschule für Technik und Wirtschaft Berlin University of Applied Sciences;Polzunov Altai State Technical University;

关键词: cps;    keymaera;    proof contracts;    verification;    hybrid systems;    usability;    interactive provers;   

DOI  :  10.18255/1818-1015-2018-5-465-480

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown