Deriving Safety Cases from Automatically Constructed Proofs

Basir, Nurlida; Denney, Ewen; Fischer, Bernd

Formal proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because the formalism in which they are constructed and encoded is usually machine-oriented, and they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to develop safety cases that correspond to formal proofs found by automated theorem provers and reveal the underlying argumentation structure and top-level assumptions. We concentrate on natural deduction style proofs, which are closer to human reasoning than resolution proofs, and show how to construct the safety cases by covering the natural deduction proof tree with corresponding safety case fragments. We also abstract away logical book-keeping steps, which reduces the size of the constructed safety cases. We show how the approach can be applied to the proofs found by the Muscadet prover.

Document ID

20100023348

Acquisition Source

Ames Research Center

Document Type

Conference Paper

Authors

Date Acquired

August 24, 2013

Publication Date

October 26, 2009

Subject Category

Report/Patent Number

Meeting Information

Meeting: 4th IET International Conference on System Safety

Location: London

Country: United Kingdom

Start Date: October 26, 2009

Funding Number(s)

Distribution Limits

Public

Public Use Permitted.

Available Downloads

Name

Type

20100023348.pdf

STI

No Preview Available

NTRS

NTRS - NASA Technical Reports Server

Available Downloads

Related Records