Semantic Analysis of Assurance Cases Using s(CASP)

Anitha Murugesan, Isaac Hong Wong, Robert Stroud, Joaquin 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.

Superseded by Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP

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 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},
  month = jul,
  address = {London, UK},
  year={2023},
  volume={3437},
  series={CEUR Workshop Proceedings}
}
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