Semantic Analysis of Assurance Cases Using s(CASP)

Anitha Murugesan, Isaac Hong Wong, Robert Stroud, Joaquín Arias, Elmer Salazar, Gopal Gupta, Robin Bloomfield, Srivatsan Varadarajan, and John Rushby

Presented at ICLP 2023 Workshop on Goal-Directed Execution of Answer Set Programs (GDE), London UK, July 2023.

Abstract

The use of assurance cases is gaining popularity, particularly in the safety-critical system industry, as an organized approach to submitting documentation for the safety and security certification of systems. However, these arguments can become overwhelming and complicated, even for moderately complex systems. Therefore, there is a compelling requirement to develop new automation strategies that can aid in creating and assessing assurance cases. Existing assurance-case tools primarily automate syntactic analysis, focusing on structural completeness, while providing limited or no support for semantically evaluating the logical aspects of the assurance case.

In prior work, we introduced a framework called Assurance 2.0, which aims to enhance the rigor of assurance cases by emphasizing the reasoning process, evidence utilized, and explicit identification of counter-claims (defeaters) and counter-evidence. In this paper, we present a new approach to enhancing Assurance 2.0 by incorporating semantic rule-based analysis capabilities. Firstly, we systematically convert the assurance case into Prolog predicates and constraints. Then, leveraging the analysis capabilities of the s(CASP), a goal-directed top-down solver for Constraints Answer Set Programs, we evaluate the semantic properties of assurance cases, including logical consistency, completeness, and indefeasibility. The application of these analyses provides both authors and evaluators with higher confidence when assessing the assurance case.

PDF

BibTeX Entry

@inproceedings{Murugesan-etal:GDE23,
  booktitle={International Conference on Logic Programming 2023
    Workshops: Goal-Directed Execution of Answer Set Programs (GDE)},
  title = {Semantic Analysis of Assurance Cases Using {s(CASP)}},
  author = {Anitha Murugesan and others},
  month = jul,
  address = {London, UK},
  year={2023},
  volume={3437},
  series={CEUR Workshop Proceedings},
  publisher = {}
}

alternative full author list:

author = {Anitha Murugesan and Isaac Hong Wong and Robert Stroud and
Joaquín Arias and Elmer Salazar and Gopal Gupta and Robin Bloomfield
and Srivatsan Varadarajan and John Rushby},
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page