Simon Foster

Simon Foster, Yakoub Nemouchi, Mario Gleirscher et al.

Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as the use of formal methods 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, called Isabelle/SACM, supporting the computer-assisted construction of assurance cases compliant with the OMG Structured Assurance Case Meta-Model. The use of Isabelle/SACM guarantees well-formedness, consistency, and traceability of assurance cases, and allows a tight integration of formal and informal evidence of various provenance. In particular, Isabelle brings a diverse range of automated verification techniques that can provide evidence. To validate our approach, we present a substantial case study based on the Tokeneer secure entry system benchmark. We embed its functional specification into Isabelle, verify its security requirements, and form a modular security case in Isabelle/SACM that combines the heterogeneous artifacts. We thus show that Isabelle is a suitable platform for critical systems assurance.

Yakoub Nemouchi, Simon Foster, Mario Gleirscher et al.

Assurance cases are often required as a means to certify a critical system. Use of formal methods in assurance can improve automation, and overcome problems with ambiguity, faulty reasoning, and inadequate evidentiary support. However, assurance cases can rarely be fully formalised, as the use of formal methods is contingent on models validated by informal processes. Consequently, we need assurance techniques that support both formal and informal artifacts, with explicated inferential links and assumptions that can be checked by evaluation. Our contribution is a mechanical framework for developing assurance cases with integrated formal methods based in the Isabelle system. We demonstrate an embedding of the Structured Assurance Case Meta-model (SACM) using Isabelle/DOF, and show how this can be linked to formal analysis techniques originating from our verification framework, Isabelle/UTP. We validate our approach by mechanising a fragment of the Tokeneer security case, with evidence supplied by formal verification.

Luis Diogo Couto, Simon Foster, Richard Payne

This paper explores verification of constituent systems within the context of the Symphony tool platform for Systems of Systems (SoS). Our SoS modelling language, CML, supports various contractual specification elements, such as state invariants and operation preconditions, which can be used to specify contractual obligations on the constituent systems of a SoS. To support verification of these obligations we have developed a proof obligation generator and theorem prover plugin for Symphony. The latter uses the Isabelle/HOL theorem prover to automatically discharge the proof obligations arising from a CML model. Our hope is that the resulting proofs can then be used to formally verify the conformance of each constituent system, which is turn would result in a dependable SoS.