Anzeige
Erschienen in:
2017 | OriginalPaper | Buchkapitel
Qualification of a Model Checker for Avionics Software Verification
verfasst von : Lucas Wagner, Alain Mebsout, Cesare Tinelli, Darren Cofer, Konrad Slind
Erschienen in: NASA Formal Methods
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
Formal methods tools have been shown to be effective at finding defects in safety-critical systems, including avionics systems in commercial aircraft. The publication of DO-178C and the accompanying formal methods supplement DO-333 provide guidance for aircraft manufacturers and equipment suppliers who wish to obtain certification credit for the use of formal methods for software development and verification.
However, there are still a number of issues that must be addressed before formal methods tools can be injected into the design process for avionics systems. DO-178C requires that a tool used to meet certification objectives be qualified to demonstrate that its output can be trusted. The qualification of formal methods tools is a relatively new concept presenting unique challenges for both formal methods researchers and software developers in the aerospace industry.
This paper presents the results of a recent project studying the qualification of formal methods tools. We have identified potential obstacles to their qualification and proposed mitigation strategies. We have conducted two case studies based on different qualification approaches for an open source formal verification tool, the Kind 2 model checker. The first case study produced a qualification package for Kind 2. The second demonstrates the feasibility of independently verifying the output of Kind 2 through the generation of proof certificates and verifying these certificates with a qualified proof checker, in lieu of qualifying the model checker itself.