Interactive verification of cyber-physical systems: Interfacing Averest and KeYmaera
- Resource Type
- Conference
- Authors
- Li, Xian; Bauer, Kerstin; Schneider, Klaus
- Source
- 2013 Federated Conference on Computer Science and Information Systems Computer Science and Information Systems (FedCSIS), 2013 Federated Conference on. :1405-1412 Sep, 2013
- Subject
- Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Computing and Processing
Robotics and Control Systems
Signal Processing and Analysis
Transportation
Semantics
Computers
Computational modeling
Computer languages
Model checking
Hardware
- Language
Verification is one of the essential topics in research of cyber-physical systems. Due to the combination of discrete and continuous dynamics, most verification problems are undecidable and need to be dealt with by various kinds abstraction techniques. As systems grow larger and larger, most verification problems are difficult even for purely discrete systems. One way to address this problem is the use of interactive verification. Recently, this approach has also been considered by cyber-physical verification tools like KeYmaera and other classical theorem provers.