Formal methods tools are expected to play a larger role in implementing and certifying safety-critical systems over the next decade. Updated certification guidance for airborne software was recently published in RTCA DO-178C. A companion document, DO-333, the formal methods supplement, allows applicants to receive certification credit for verification conducted using formal methods. DO-330, Software Tool Qualification Considerations, provides guidance for developers and users of software tools for safety-critical domains. DO-330 qualification of formal methods tools, and more generally, the larger question of formal methods tool dependability, forms a largely unexplored area of study.
This NASA-funded project investigated what sorts of assurances are necessary and appropriate to justify the application of formal methods tools throughout all phases of design in real safety-critical settings. We produced practical examples on how to qualify typical formal verification tools in each of the three categories identified in DO-333 (theorem proving, model checking, and abstract interpretation) and explored promising new approaches to the qualification of formal methods tools. We produced the qualification artifacts for an open source formal verification tool, the Kind model checker. We also investigated the feasibility of independently verifying tool outputs through the generation of a proof certificate and verification of the certificate with a qualified proof checker.
As part of the project, we organized a Dagstuhl Seminar to explore the subject of tool qualification with the formal methods research community.
Final results from the project are available as a NASA Contractor Report, along with the case study qualification tests and tools.