A Generic Goal-Based Certification Argument for the Justification of Formal Analysis

Formal methods are powerful specification and verification techniques for establishing high confidence in safety-critical systems. However, there are a number of concerns about the use of evidence generated from formal methods, when used in place of conventional testing, for satisfying certain certification objectives. In this paper, we address this issue by reviewing two certification documents, DO-178B and the UK Defence Standard 00-56, focusing on their approach to accepting formal analytical evidence. We also present a generic goal-based safety case that can be instantiated to facilitate the justification and presentation of formal analysis to the certification authorities. The safety case is based on claims about (1) the achievement of the intents of the certification objectives, (2) the demonstration of the trustworthiness of formal analysis and (3) the practical feasibility of deploying formal methods within a specific project.