Formal verification of safety-critical hybrid systems

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.

Download Full-text

A Formal Verification Methodology for DDD Mode Pacemaker Control Programs

Journal of Electrical and Computer Engineering ◽

10.1155/2015/939028 ◽

2015 ◽

Vol 2015 ◽

pp. 1-10 ◽

Cited By ~ 5

Author(s):

Sana Shuja ◽

Sudarshan K. Srinivasan ◽

Shaista Jabeen ◽

Dharmakeerthi Nawarathna

Keyword(s):

Formal Verification ◽

Control Program ◽

Formal Specifications ◽

Object Code ◽

Correctness Proof ◽

Safety Critical ◽

Control Programs ◽

Control Functions ◽

Verification Process ◽

Verification Methodology

Pacemakers are safety-critical devices whose faulty behaviors can cause harm or even death. Often these faulty behaviors are caused due to bugs in programs used for digital control of pacemakers. We present a formal verification methodology that can be used to check the correctness of object code programs that implement the safety-critical control functions of DDD mode pacemakers. Our methodology is based on the theory of Well-Founded Equivalence Bisimulation (WEB) refinement, where both formal specifications and implementation are treated as transition systems. We develop a simple and general formal specification for DDD mode pacemakers. We also develop correctness proof obligations that can be applied to validate object code programs used for pacemaker control. Using our methodology, we were able to verify a control program with millions of transitions against the simple specification with only 10 transitions. Our method also found several bugs during the verification process.

Download Full-text

Model Checking for SpaceWire Error Detection Module

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.241-244.3020 ◽

2012 ◽

Vol 241-244 ◽

pp. 3020-3025

Author(s):

Ling Ling Dong ◽

Yong Guan ◽

Xiao Juan Li ◽

Zhi Ping Shi ◽

Jie Zhang ◽

...

Keyword(s):

Model Checking ◽

Formal Verification ◽

Temporal Logic ◽

Error Detection ◽

System Model ◽

Linear Search ◽

Kripke Structure ◽

Mathematical Methods ◽

Safety Critical ◽

Correctness Of Programs

Considerable attention has been devoted to prove the correctness of programs. Formal verification overcomes the incompleteness by applying mathematical methods to verify a design. SpaceWire is a well known communication standard. For safety-critical applications an approach is needed to validate the completeness of SpareWire design. This paper addresses formal verification of SpareWire error detection module. The system model was constructed by Kripke structure, and the properties were presented by linear temporal logic (LTL). Compared the verification of LTL with CTL (branch temporal logic), LTL properties could improve the verification efficiency due to its linear search. The error priority was checked using simulation guided by model checking. After some properties were modified, all possible behaviors of the module satisfied the specification. This method realizes complete validation of the error detection module.

Download Full-text

Formal verification of safety-critical systems

Software Practice and Experience ◽

10.1002/spe.4380200804 ◽

1990 ◽

Vol 20 (8) ◽

pp. 799-821 ◽

Cited By ~ 18

Author(s):

Louise E. Moser ◽

P. M. Melliar-Smith

Keyword(s):

Formal Verification ◽

Critical Systems ◽

Safety Critical ◽

Safety Critical Systems

Download Full-text

ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics

10.29007/73mb ◽

2018 ◽

Author(s):

Matthias Althoff ◽

Stanley Bak ◽

Xin Chen ◽

Chuchu Fan ◽

Marcelo Forets ◽

...

Keyword(s):

Formal Verification ◽

Hybrid Systems ◽

Benchmark Problems ◽

Safety Verification ◽

Alphabetical Order ◽

Friendly Competition

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In its second edition, 9 tools have been applied to solve six different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, CORA/SX, C2E2, Flow*, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

Download Full-text

ARCH-COMP18 Category Report: Hybrid Systems with Piecewise Constant Dynamics

10.29007/p11g ◽

2018 ◽

Author(s):

Goran Frehse ◽

Alessandro Abate ◽

Dieky Adzkiya ◽

Lei Bu ◽

Mirco Giacobbe ◽

...

Keyword(s):

Formal Verification ◽

Hybrid Systems ◽

Benchmark Problems ◽

Safety Verification ◽

Railway Network ◽

Piecewise Constant ◽

Friendly Competition

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this second edition, five tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, PHAVer, PHAVer-lite, and VeriSiMPL. Compared to last year, a new tool has participated (PHAVer-lite) and a benchmark has been made more complex (Dutch Railway Network). The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

Download Full-text

ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

10.29007/zkf6 ◽

2020 ◽

Author(s):

Luca Geretti ◽

Julien Alexandre Dit Sandretto ◽

Matthias Althoff ◽

Luis Benet ◽

Alexandre Chapoutot ◽

...

Keyword(s):

Nonlinear Dynamics ◽

Formal Verification ◽

Hybrid Systems ◽

Reachability Analysis ◽

Current Status ◽

Benchmark Problems ◽

Hybrid Dynamics ◽

Friendly Competition

We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.

Download Full-text