Abstract-We describe a generic approach for automatically integrating the output generated from a formal method/tool into a software safety assurance case, as an evidence argument, by (a) encoding the underlying reasoning as a safety case pattern, and (b) instantiating it using the data produced from the method/tool. We believe this approach not only improves the trustworthiness of the evidence generated from a formal method/tool, by explicitly presenting the reasoning and mechanisms underlying its genesis, but also provides a way to gauge the suitability of the evidence in the context of the wider assurance case. We illustrate our work by application to a real example-an unmanned aircraft systemwhere we invoke a formal code analysis tool from its autopilot software safety case, automatically transform the verification output into an evidence argument, and then integrate it into the former.
Similar work in REF describes patterns for using proofs within a safety case and automation for generating portions of the proof as a part of the safety case.
Evidence arguments for using formal methods in software certification
2013 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)
2013 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)
Computer Science