Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study

Simon David Foster; Yakoub Nemouchi; Colin O'Halloran; Nick Tudor; Karen Stephenson

doi:10.1145/3372020.3391559

Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study

Simon David Foster, Yakoub Nemouchi, Colin O'Halloran, Nick Tudor, Karen Stephenson

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Isabelle/SACM is a tool for automated construction of model-based assurance cases with integrated formal methods, based on the Isabelle proof assistant. Assurance cases show how a system is safe to operate, through a human comprehensible argument demonstrating that the requirements are satisfied, using evidence of various provenances. They are usually required for certification of critical systems, often with evidence that originates from formal methods. Automating assurance cases increases rigour, and helps with maintenance and evolution. In this paper we apply Isabelle/SACM to a fragment of the assurance case for an autonomous underwater vehicle demonstrator. We encode the metric unit system (SI) in Isabelle, to allow modelling requirements and state spaces using physical units. We develop a behavioural model in the graphical RoboChart state machine language, embed the artifacts into Isabelle/SACM, and use it to demonstrate satisfaction of the requirements.

Original language	English
Title of host publication	FormaliSE '20
Subtitle of host publication	Proceedings of the 8th International Conference on Formal Methods in Software Engineering
Publisher	ACM
ISBN (Print)	9781450370714
DOIs	https://doi.org/10.1145/3372020.3391559
Publication status	Published - 7 Oct 2020

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.

Access to Document

10.1145/3372020.3391559

FormaliSE2020
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.
Accepted author manuscript, 1.38 MBLicence: Unspecified

Cite this

@inproceedings{b7f38d0643414ae08c21a6fcd5e3ebc3,

title = "Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study",

abstract = "Isabelle/SACM is a tool for automated construction of model-based assurance cases with integrated formal methods, based on the Isabelle proof assistant. Assurance cases show how a system is safe to operate, through a human comprehensible argument demonstrating that the requirements are satisfied, using evidence of various provenances. They are usually required for certification of critical systems, often with evidence that originates from formal methods. Automating assurance cases increases rigour, and helps with maintenance and evolution. In this paper we apply Isabelle/SACM to a fragment of the assurance case for an autonomous underwater vehicle demonstrator. We encode the metric unit system (SI) in Isabelle, to allow modelling requirements and state spaces using physical units. We develop a behavioural model in the graphical RoboChart state machine language, embed the artifacts into Isabelle/SACM, and use it to demonstrate satisfaction of the requirements.",

author = "Foster, {Simon David} and Yakoub Nemouchi and Colin O'Halloran and Nick Tudor and Karen Stephenson",

note = "This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details.",

year = "2020",

month = oct,

day = "7",

doi = "10.1145/3372020.3391559",

language = "English",

isbn = "9781450370714",

booktitle = "FormaliSE '20",

publisher = "ACM",

address = "United States",

}

TY - GEN

T1 - Formal Model-Based Assurance Cases in Isabelle/SACM

T2 - An Autonomous Underwater Vehicle Case Study

AU - Foster, Simon David

AU - Nemouchi, Yakoub

AU - O'Halloran, Colin

AU - Tudor, Nick

AU - Stephenson, Karen

N1 - 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.

PY - 2020/10/7

Y1 - 2020/10/7

N2 - Isabelle/SACM is a tool for automated construction of model-based assurance cases with integrated formal methods, based on the Isabelle proof assistant. Assurance cases show how a system is safe to operate, through a human comprehensible argument demonstrating that the requirements are satisfied, using evidence of various provenances. They are usually required for certification of critical systems, often with evidence that originates from formal methods. Automating assurance cases increases rigour, and helps with maintenance and evolution. In this paper we apply Isabelle/SACM to a fragment of the assurance case for an autonomous underwater vehicle demonstrator. We encode the metric unit system (SI) in Isabelle, to allow modelling requirements and state spaces using physical units. We develop a behavioural model in the graphical RoboChart state machine language, embed the artifacts into Isabelle/SACM, and use it to demonstrate satisfaction of the requirements.

AB - Isabelle/SACM is a tool for automated construction of model-based assurance cases with integrated formal methods, based on the Isabelle proof assistant. Assurance cases show how a system is safe to operate, through a human comprehensible argument demonstrating that the requirements are satisfied, using evidence of various provenances. They are usually required for certification of critical systems, often with evidence that originates from formal methods. Automating assurance cases increases rigour, and helps with maintenance and evolution. In this paper we apply Isabelle/SACM to a fragment of the assurance case for an autonomous underwater vehicle demonstrator. We encode the metric unit system (SI) in Isabelle, to allow modelling requirements and state spaces using physical units. We develop a behavioural model in the graphical RoboChart state machine language, embed the artifacts into Isabelle/SACM, and use it to demonstrate satisfaction of the requirements.

U2 - 10.1145/3372020.3391559

DO - 10.1145/3372020.3391559

M3 - Conference contribution

SN - 9781450370714

BT - FormaliSE '20

PB - ACM

ER -