NTRS - NASA Technical Reports Server

Back to Results
formal methods tool qualificationFormal 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.
Document ID
Document Type
Contractor Report (CR)
Wagner, Lucas G.
(Rockwell Collins, Inc. Cedar Rapids, IA, United States)
Cofer, Darren
(Rockwell Collins, Inc. Cedar Rapids, IA, United States)
Slind, Konrad
(Rockwell Collins, Inc. Cedar Rapids, IA, United States)
Tinelli, Cesare
(Iowa Univ. Iowa City, IA, United States)
Mebsout, Alain
(Iowa Univ. Iowa City, IA, United States)
Date Acquired
March 28, 2017
Publication Date
February 1, 2017
Subject Category
Numerical Analysis
Report/Patent Number
Funding Number(s)
WBS: WBS 999182.
Distribution Limits
Public Use Permitted.

Available Downloads

NameType 20170002594.pdf STI