NASA Logo

NTRS

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
20170002594
Document Type
Contractor Report (CR)
Authors
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
NF1676L-25881
NASA/CR-2017-219371
Funding Number(s)
WBS: WBS 999182.02.85.07.01
CONTRACT_GRANT: NNL14AA06C
Distribution Limits
Public
Copyright
Public Use Permitted.

Available Downloads

NameType 20170002594.pdf STI