Report
Formal Methods Tool Qualification
Langley Research Center
02/2017
Abstract
Formal methods tools have been shown to be effective at finding defects in safety-critical digital systems including avionics systems. The publication of DO-178C and the accompanying formal methods supplement DO-333 allows applicants to obtain certification credit for the use of formal methods without providing justification for them as an alternative method. This project conducted an extensive study of existing formal methods tools, identifying obstacles to their qualification and proposing mitigations for those obstacles. Further, it interprets the qualification guidance for existing formal methods tools and provides case study examples for open source tools. This project also investigates the feasibility of verifying formal methods tools by generating proof certificates which capture proof of the formal methods tool's claim, which can be checked by an independent, proof certificate checking tool. Finally, the project investigates the feasibility of qualifying this proof certificate checker, in the DO-330 framework, in lieu of qualifying the model checker itself.
Details
- Title: Subtitle
- Formal Methods Tool Qualification
- Creators
- Lucas G. Wagner - Rockwell Collins, IncDarren Cofer - Rockwell Collins, IncKonrad Slind - Rockwell Collins, IncCesare Tinelli - Iowa UnivAlain Mebsout - Iowa Univ
- Resource Type
- Report
- Publisher
- Langley Research Center
- Number of pages
- 45 pages
- Comment
- NASA/CR–2017-219371
- Language
- English
- Date published
- 02/2017
- Description audience
- PUBLIC
- Academic Unit
- Computer Science
- Record Identifier
- 9984410859402771
Metrics
1 Record Views