Formal verification of safety-critical software using SPARK

2021 ◽  
pp. 31-48
Author(s):  
Laura Humphrey ◽  
Ryan Baity ◽  
Kenneth Hopkinson
Keyword(s):  
Formal Verification ◽  
Safety Critical

scholarly journals A Formal Verification Methodology for DDD Mode Pacemaker Control Programs

2015 ◽  
Vol 2015 ◽  
pp. 1-10 ◽  
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.

Model Checking for SpaceWire Error Detection Module

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.

Formal verification of safety-critical systems

1990 ◽  
Vol 20 (8) ◽  
pp. 799-821 ◽  
Author(s):  
Louise E. Moser ◽  
P. M. Melliar-Smith
Keyword(s):  
Formal Verification ◽  
Critical Systems ◽  
Safety Critical ◽  
Safety Critical Systems

scholarly journals A Formal Verification Method of Compilation Based on C Safety Subset

2021 ◽  
Vol 2021 ◽  
pp. 1-10
Author(s):  
Yu Tan ◽  
Dianfu Ma ◽  
Lei Qiao
Keyword(s):  
Wireless Communication ◽  
Formal Verification ◽  
Communication Systems ◽  
System Development ◽  
Axiom System ◽  
Proof Complexity ◽  
Verification Method ◽  
Safety Critical ◽  
Algorithm Efficiency ◽  
Verification Methods

With the rapid increase in the number of wireless terminals and the openness of wireless networks, the security of wireless communication is facing serious challenges. The safety and security of computer communication have always been a research hotspot, especially the wireless communication that still has a more complex architecture which leads to more safety problems in the communication system development. In recent years, more and more wireless communication systems are applied in the safety-critical field which tends to need high safety guarantees. A compiler is an important tool for system development, and its safety and reliability have an important impact on the development of safety-critical software. As the strictest method, formal verification methods have been widely paid attention to in compiler verification, but the current formal verification methods have some problems, such as high proof complexity, weak verification ability, and low algorithm efficiency. In this paper, a compiler formal verification method based on safety C subsets is proposed. By abstracting the concept of C grammar units from safety C subsets, the formal verification of the compiler is transformed into the verification of limited C grammar units. In this paper, an axiom system of first-order logic and special axioms are introduced. On this axiom system, the semantic consistency verification of C grammar unit and target code pattern is completed by means of theorem proving, and the formal verification of the compiler is completed.

Accessible formal verification for safety-critical hardware design

2006 ◽  
Author(s):  
J. Lach ◽  
S. Bingham ◽  
C. Elks ◽  
T. Lenhart ◽  
Thuy Nguyen ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hardware Design ◽  
Safety Critical

Hamilton–Jacobi Reachability: Some Recent Theoretical Advances and Applications in Unmanned Airspace Management

2018 ◽  
Vol 1 (1) ◽  
pp. 333-358 ◽  
Author(s):  
Mo Chen ◽  
Claire J. Tomlin
Keyword(s):  
Nonlinear Systems ◽  
Everyday Life ◽  
Formal Verification ◽  
Autonomous Systems ◽  
High Dimensional ◽  
System Decomposition ◽  
Computational Burden ◽  
Safety Critical ◽  
Verification Tool ◽  
Difficult Challenge

Autonomous systems are becoming pervasive in everyday life, and many of these systems are complex and safety-critical. Formal verification is important for providing performance and safety guarantees for these systems. In particular, Hamilton–Jacobi (HJ) reachability is a formal verification tool for nonlinear and hybrid systems; however, it is computationally intractable for analyzing complex systems, and computational burden is in general a difficult challenge in formal verification. In this review, we begin by briefly presenting background on reachability analysis with an emphasis on the HJ formulation. We then present recent work showing how high-dimensional reachability verification can be made more tractable by focusing on two areas of development: system decomposition for general nonlinear systems, and traffic protocols for unmanned airspace management. By tackling the curse of dimensionality, tractable verification of practical systems is becoming a reality, paving the way for more pervasive and safer automation.

Sign in / Sign up

Export Citation Format

Share Document