Qualification of Formal Methods Tools under DO-330

Study led by Rockwell Collins

RTCA DO-333 has enabled the use of formal methods technology to create certification evidence. When software tools are used in the creation of such evidence, it is generally necessary to qualify the tools to ensure they are dependable. A second RTCA document, DO-330, provides guidance on how to structure a tool qualification package. Given that formal methods tools have rarely undergone qualification in the past, NASA Langley Research Center, with encouragement from the FAA, decided to investigate the general feasibility of qualifying formal methods tools.

During 2014-2016, a study task was performed by Rockwell Collins under a contract awarded by NASA Langley. A subcontract to the University of Iowa contributed additional research expertise. The products of this study include several reports and a collection of case study artifacts from a simulated qualification of Kind 2, a model checking tool. These results have been made publicly available as an aid to both certification authorities and applicants. A NASA Contractor Report, whose abstract is shown below, summarizes the results achieved under the contract.

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.

Downloads

• The NASA Contractor Report, Formal Methods Tool Qualification, summarizes issues pertinent to formal methods tool qualification, and describes the qualification case studies performed under the contract (NASA/CR-2017-219371, February 2017, 45 pages).
• Detailed reports on individual study tasks within this project are also available. Included are several Tool Qualification Plans (TQP) for representative tools. These documents have been collected and packaged as a zip file (7 MB).
• Readers wishing to examine or run the case study qualification tests can download the following zip files.
  • Tests for the Kind 2 model checker (1 MB).
  • Tests for the Kind 2 proof certificate checker (136 MB).
  • Tools for running the tests cases (94 MB).

Acknowledgements

These research reports and case study materials were produced by Lucas Wagner (principal investigator), Darren Cofer and Konrad Slind of Rockwell Collins; and Cesare Tinelli and Alain Mebsout of the University of Iowa.

The tag identifies links that are outside the NASA domain.