Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

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

TL;DR

The paper addresses the challenge that assurance cases, while structurally organized, often lack rigorous semantic coherence. It extends the Assurance 2.0 framework by translating cases into ASP and applying semantic analysis with the s(CASP) solver to assess properties like indefeasibility, theory correctness, and consistency. Key contributions include a formal Object-Property-Environment mapping, an automated ASP transformation pipeline, defined semantic properties, and a set of s(CASP)-driven analyses demonstrated on aircraft/nuclear-relevant domains. The approach enhances explainability, enables automated validation, and improves confidence in assurance cases, with future work focusing on large-scale cases and LLM-assisted semantics.

Abstract

Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools focus on automating structural aspects, they lack the ability to fully assess the semantic coherence and correctness of the assurance arguments. In prior work, we introduced the Assurance 2.0 framework that prioritizes the reasoning process, evidence utilization, and explicit delineation of counter-claims (defeaters) and counter-evidence. In this paper, we present our approach to enhancing Assurance 2.0 with semantic rule-based analysis capabilities using common-sense reasoning and answer set programming solvers, specifically s(CASP). By employing these analysis techniques, we examine the unique semantic aspects of assurance cases, such as logical consistency, adequacy, indefeasibility, etc. The application of these analyses provides both system developers and evaluators with increased confidence about the assurance case.

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

TL;DR

The paper addresses the challenge that assurance cases, while structurally organized, often lack rigorous semantic coherence. It extends the Assurance 2.0 framework by translating cases into ASP and applying semantic analysis with the s(CASP) solver to assess properties like indefeasibility, theory correctness, and consistency. Key contributions include a formal Object-Property-Environment mapping, an automated ASP transformation pipeline, defined semantic properties, and a set of s(CASP)-driven analyses demonstrated on aircraft/nuclear-relevant domains. The approach enhances explainability, enables automated validation, and improves confidence in assurance cases, with future work focusing on large-scale cases and LLM-assisted semantics.

Abstract

Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools focus on automating structural aspects, they lack the ability to fully assess the semantic coherence and correctness of the assurance arguments. In prior work, we introduced the Assurance 2.0 framework that prioritizes the reasoning process, evidence utilization, and explicit delineation of counter-claims (defeaters) and counter-evidence. In this paper, we present our approach to enhancing Assurance 2.0 with semantic rule-based analysis capabilities using common-sense reasoning and answer set programming solvers, specifically s(CASP). By employing these analysis techniques, we examine the unique semantic aspects of assurance cases, such as logical consistency, adequacy, indefeasibility, etc. The application of these analyses provides both system developers and evaluators with increased confidence about the assurance case.
Paper Structure (11 sections, 9 figures, 2 tables)

This paper contains 11 sections, 9 figures, 2 tables.

Table of Contents

  1. Formalism of Assurance Statements
  2. Transformation into ASP
  3. Modeling Semantic Properties
  4. Semantic Reasoning using s(CASP)
  5. Indefeasibly Justified:
  6. Theory Application Correctness:
  7. Property-Object-Environment Consistency:
  8. Adequacy:
  9. Completeness:
  10. Harmonious Coexistence of Theories:
  11. Conclusion

Figures (9)

  • Figure 4: Objects-Properties-Environments Formalism and LLM Support
  • Figure 5: Object-Property Relationships
  • Figure 6: Snippet of export of Arducopter Assurance Case into ASP.
  • Figure 7: Semantic Analysis Option in ASCE Interface
  • Figure 8: Positive and Negative Query Exported from Top-level Claim Node
  • ...and 4 more figures