NTRS - NASA Technical Reports Server
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.
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)
March 28, 2017
February 1, 2017
WBS: WBS 999182.02.85.07.01
Public Use Permitted.
Available Downloads 20170002594.pdf STI