Integrated Formal Methods for Constructing Assurance Cases

摘要

The use of formal methods in verification activities is well established in various dedicated safety standards. Deficits in the verification process may have a negative impact on the confidence of verification results. Safety standards promote the use of integrated formal methods when a single method cannot achieve the verification objective without specifying how. In this paper, we take on the problem of using outputs from integrated formal methods as evidence in assurance cases, which are used in certification of safety-critical systems. We first present two workflows that employ integrated formal methods - code review workflow and code coverage workflow - corresponding to two of the most important activities of the verification phase. Then, we show how each workflow and the outputs from its integrated formal methods can be used in creating an assurance argument. These assurance arguments offer evidence for undeveloped goals identified in previous works from the field.