Approaches to the Formal Verification of Hybrid Systems

2001 ◽  
Vol 49 (2/2001) ◽  
Author(s):  
St. Kowalewski ◽  
P. Herrmann ◽  
Sebastian Engell ◽  
R. Huuck ◽  
H. Krumm ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Verification Of Hybrid Systems

scholarly journals A Benchmark for Component-based Hybrid Systems Safety Verification

10.29007/9jm3 ◽  
2018 ◽  
Author(s):  
Andreas Müller ◽  
Stefan Mitsch ◽  
Werner Retschitzegger ◽  
Wieland Schwinger ◽  
André Platzer
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Case Studies ◽  
Entire System ◽  
Safety Properties ◽  
System Safety ◽  
Guarantee System ◽  
Natural Components ◽  
Verification Of Hybrid Systems ◽  
Potential Remedy

At scale, formal verification of hybrid systems is challenging, but a potential remedy is the observation that systems often come with a number of natural components with certain local responsibilities. Ideally, such a compartmentalization into more manageable components also translates to hybrid systems verification, so that safety properties about the whole system can be derived from local verification results. We propose a benchmark consisting of a sequence of three case studies, where components interact to achieve system safety. The baseline for the benchmark is the verification effort from a monolithic fashion (i.e., the entire system without splitting it into components). We describe how to split the system models used in these case studies into components with local responsibilities, and what is expected about their interaction to guarantee system safety. The benchmark can be used to assess the performance, automation, and verification features of component-based verification approaches.

scholarly journals ARCH-COMP17 Repeatability Evaluation Report

10.29007/7hvk ◽  
2018 ◽  
Author(s):  
Taylor T. Johnson
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Evaluation Report ◽  
Standard Practice ◽  
Friendly Competition

This report presents the results of the repeatability evaluation for a friendly competition for formal verification of continuous and hybrid systems. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, thirteen tools have been applied to solve benchmark problems for the six competition categories, of which, ten tools were evaluated and passed the repeatability evaluation. The repeatability results represent a snapshot of the current landscape of tools and the types of benchmarks for which they are particularly suited and for which others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing being repeatable. These re- sults probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.

Sign in / Sign up

Export Citation Format

Share Document