Qualification of Formal Methods Tools under DO-330

Study Led by Kestrel Technology

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 Kestrel Technology under a contract awarded by NASA Langley. Subcontracts to Honeywell Aerospace Advanced Technology and Smart Information Flow Technologies (SIFT) contributed additional research expertise. The products of this study include several reports and a collection of case study artifacts from simulated qualifications of Java PathFinder (JPF), a model checking tool, and CodeHawk, an abstract interpretation engine for static analysis tools. 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

This is the Final Report of a research project to investigate issues and provide guidance for the qualification of formal methods tools under the DO-330 qualification process. It consisted of three major subtasks spread over two years: 1) an assessment of theoretical soundness issues that may affect qualification for three categories of formal methods tools, 2) a case study simulating the DO-330 qualification of two actual tool sets, and 3) an investigation of risk mitigation strategies that might be applied to chains of such formal methods tools in order to increase confidence in their certification of airborne software.

Downloads

• The NASA Contractor Report, Formal Assurance Certifiable Tooling Strategy Final Report, summarizes issues pertinent to formal methods tool qualification, and describes the qualification case studies performed under the contract (NASA/CR-2017-219372, February 2017, 36 pages).
• Detailed reports on individual study tasks within this project are also available. These documents have been collected and packaged as a zip file (2.5 MB).
• Readers wishing to examine the case study documents can download the following zip files.
  • Qualification documents for Java PathFinder (JPF) (1.5 MB).
  • Qualification documents for CodeHawk (2 MB).

Acknowledgements

These research reports and case study materials were produced by Eric Bush (principal investigator) of Kestrel Technology; Devesh Bhatt, David Oglesby, and Anitha Murugesan of Honeywell Aerospace Advanced Technology; and Eric Engstrom, Joe Mueller, and Michael Pelican of Smart Information Flow Technologies.

The tag identifies links that are outside the NASA domain.