Isabelle/SACM

Isabelle/SACM is an implementation of the Structured Assurance Case Meta-Model (SACM) in Isabelle.

What is SACM?

SACM is an OMG standard meta-model for expressing machine readable assurance cases in terms of arguments, artifacts (including evidence), and terminology. It unifies a number of existing assurance case notations, including GSN and CAE.

What is Isabelle/SACM?

Isabelle/SACM allows the elements of SACM, including claims, inferences, and artifacts, to be created as part of the Isabelle document model, and linked to diverse formal verification results. It is intended as a platform for computer-aided assurance cases with integrated formal methods. It consists of both the meta-model backend, and frontend interactive DSL for composing assurance cases.

Below is a screenshot from Isabelle/SACM showing a fragment of a simple assurance case that demonstrates that a number of hazards have been mitigated.