By the same authors

Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Full text download(s)

Links

Author(s)

Department/unit(s)

Publication details

Title of host publicationIntegrated Formal Methods
DateAccepted/In press - 16 Sep 2019
DateE-pub ahead of print (current) - 22 Nov 2019
Pages379-398
Number of pages20
PublisherSpringer International Publishing
Volume11918
Original languageEnglish
ISBN (Electronic)9783030349684
ISBN (Print)9783030349677

Publication series

NameLNCS
PublisherSpringer

Abstract

Assurance cases (ACs) are often required to certify critical systems. The use of integrated formal methods (FMs) in assurance can improve automation, increase confidence, and overcome errant reasoning. However, ACs can rarely be fully formalised, as the use of FMs is contingent on models that are validated by informal processes. Consequently, assurance techniques should support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language for the computer-assisted construction of ACs called Isabelle/SACM. The framework guarantees well-formedness, consistency, and traceability of ACs, and allows a tight integration of formal and informal evidence of various provenance. To validate Isabelle/SACM, we present a novel formalisation of the Tokeneer benchmark, verify its security requirements, and form a mechanised AC that combines the resulting formal and informal artifacts.

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Projects

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations