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

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...

Full description

Bibliographic Details
Main Authors: Thomas Baar, Sergey Staroletov
Format: Article
Language:English
Published: Yaroslavl State University 2018-10-01
Series:Modelirovanie i Analiz Informacionnyh Sistem
Subjects:
cps
keymaera
proof contracts
verification
hybrid systems
usability
interactive provers
Online Access:https://www.mais-journal.ru/jour/article/view/752

Internet

https://www.mais-journal.ru/jour/article/view/752

Similar Items