By the same authors

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

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

Standard

Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. / Nemouchi, Yakoub; Foster, Simon David; Gleirscher, Mario; Kelly, Timothy Patrick.

Integrated Formal Methods: Proceedings of the 15th International Conference. Vol. 11918 Springer International Publishing, 2019. p. 379-398 (LNCS).

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

Harvard

Nemouchi, Y, Foster, SD, Gleirscher, M & Kelly, TP 2019, Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. in Integrated Formal Methods: Proceedings of the 15th International Conference. vol. 11918, LNCS, Springer International Publishing, pp. 379-398. <http://10.1007/978-3-030-34968-4_21>

APA

Nemouchi, Y., Foster, S. D., Gleirscher, M., & Kelly, T. P. (2019). Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. In Integrated Formal Methods: Proceedings of the 15th International Conference (Vol. 11918, pp. 379-398). (LNCS). Springer International Publishing. http://10.1007/978-3-030-34968-4_21

Vancouver

Nemouchi Y, Foster SD, Gleirscher M, Kelly TP. Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. In Integrated Formal Methods: Proceedings of the 15th International Conference. Vol. 11918. Springer International Publishing. 2019. p. 379-398. (LNCS).

Author

Nemouchi, Yakoub ; Foster, Simon David ; Gleirscher, Mario ; Kelly, Timothy Patrick. / Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. Integrated Formal Methods: Proceedings of the 15th International Conference. Vol. 11918 Springer International Publishing, 2019. pp. 379-398 (LNCS).

Bibtex - Download

@inproceedings{9b60db65c4ac4796ac0853afb245955f,
title = "Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods",
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.",
author = "Yakoub Nemouchi and Foster, {Simon David} and Mario Gleirscher and Kelly, {Timothy Patrick}",
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 = "2019",
month = nov,
day = "22",
language = "English",
isbn = "9783030349677",
volume = "11918",
series = "LNCS",
publisher = "Springer International Publishing",
pages = "379--398",
booktitle = "Integrated Formal Methods",

}

RIS (suitable for import to EndNote) - Download

TY - GEN

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

AU - Nemouchi, Yakoub

AU - Foster, Simon David

AU - Gleirscher, Mario

AU - Kelly, Timothy Patrick

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 - 2019/11/22

Y1 - 2019/11/22

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

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

M3 - Conference contribution

SN - 9783030349677

VL - 11918

T3 - LNCS

SP - 379

EP - 398

BT - Integrated Formal Methods

PB - Springer International Publishing

ER -