Book chapter
Qualification of a Model Checker for Avionics Software Verification
NASA Formal Methods, pp.404-419
Lecture Notes in Computer Science, Springer International Publishing
04/09/2017
DOI: 10.1007/978-3-319-57288-8_29
Abstract
Formal methods tools have been shown to be effective at finding defects in safety-critical systems, including avionics systems in commercial aircraft. The publication of DO-178C and the accompanying formal methods supplement DO-333 provide guidance for aircraft manufacturers and equipment suppliers who wish to obtain certification credit for the use of formal methods for software development and verification.
However, there are still a number of issues that must be addressed before formal methods tools can be injected into the design process for avionics systems. DO-178C requires that a tool used to meet certification objectives be qualified to demonstrate that its output can be trusted. The qualification of formal methods tools is a relatively new concept presenting unique challenges for both formal methods researchers and software developers in the aerospace industry.
This paper presents the results of a recent project studying the qualification of formal methods tools. We have identified potential obstacles to their qualification and proposed mitigation strategies. We have conducted two case studies based on different qualification approaches for an open source formal verification tool, the Kind 2 model checker. The first case study produced a qualification package for Kind 2. The second demonstrates the feasibility of independently verifying the output of Kind 2 through the generation of proof certificates and verifying these certificates with a qualified proof checker, in lieu of qualifying the model checker itself.
Details
- Title: Subtitle
- Qualification of a Model Checker for Avionics Software Verification
- Creators
- Lucas Wagner - Advanced Technology Center, Rockwell Collins, Cedar Rapids, USAAlain Mebsout - The University of Iowa, Iowa City, USACesare Tinelli - The University of Iowa, Iowa City, USADarren Cofer - Advanced Technology Center, Rockwell Collins, Cedar Rapids, USAKonrad Slind - Advanced Technology Center, Rockwell Collins, Cedar Rapids, USA
- Resource Type
- Book chapter
- Publication Details
- NASA Formal Methods, pp.404-419
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-57288-8_29
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 04/09/2017
- Academic Unit
- Computer Science
- Record Identifier
- 9984002301602771
Metrics
95 Record Views