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.
In recent years, there has been a growing interest in the safety-critical field to develop assurance
cases as a means of establishing credible confidence in claims made about a system, particularly
regarding its safety or security. These assurance cases typically consist of a claim that defines
the desired property, evidence supporting the design and construction of the system, and
a well-structured and persuasive argument demonstrating that the evidence is suficient to
support the claim. Unlike the traditional approach of presenting a laborious checklist of activities
performed or not performed for system assurance, assurance cases focus on creating a systematic
argumentative record. As a result, they are widely recommended as a practical alternative for
organizations seeking safety/security certification from agencies such as the FAA [
At its core, a correct assurance case is one in which the top-level claim logically follows from the composition of its sub-claims, arguments, and supporting evidence. However, even for systems of moderate complexity, assurance cases can become exceedingly large, consisting of extensive sets of arguments and a substantial body of evidence, all expressed in natural language. Consequently, both the authors and evaluators of assurance cases must diligently verify the correctness of the arguments and evidence and ensure they logically support the stated claims about the system. Unfortunately, this process is time-consuming, intellectually demanding, and prone to errors. The risk lies in the possibility of approving flawed assurance arguments and consequently certifying systems that are unsafe or insecure.
To address this challenge, researchers and practitioners worldwide have developed numerous
tools and techniques aimed at automatically analyzing specific syntactic elements of assurance
cases. These include ensuring adherence to notations, assessing structural completeness, and
conducting grammar and spell checks within the natural language descriptions [
This paper presents our approach to conducting a formal analysis of specific semantic aspects
within assurance cases. We have previously introduced Assurance 2.0 [
We begin by formally establishing the objects pertaining to the system under consideration, the properties that are asserted, and the operational environment for each claim, argument, and evidence. Although this step currently requires manual efort, we are actively investigating methods to automatically extract this information from natural language descriptions. Subsequently, we automatically convert the entire assurance case into predicates and constraints expressed in Prolog as a logic programming language. We then interface with the s(CASP) reasoning engine to systematically examine the consistency of the predicates, identifying any violations of the constraints, and assessing the completeness of the assurance arguments.
In order to illustrate the concepts of our approach and tool-suite, we will use a generic
example [
Assurance 2.0 is a modern framework to support reasoning and communication about the
behavior and trustworthiness of engineered systems and their certification. This framework adopts a
Claims-Arguments-Evidence approach, with an increased focus on the evidence presented, the
logical reasoning utilized, and the exploration and assessment of counter-claims [
Figure 1 shows an Assurance 2.0 case for the safe driver example. It has a top-level claim (blue
ellipse) that is hierarchically refined into fine-grained sub-claims (blue ellipses) via arguments
(green round-edge rectangles) that are eventually discharged by evidence (purple rectangles)
at the leaf level. The rationale for such refinements is captured in side-claims (yellow ellipses).
Further, doubts, concerns, or counter-claims on any part of the case are captured as defeaters
(red ellipses) [
Recently, Assurance 2.0 is augmented with the notion of theories [
To a large extent, assurance cases rely primarily on free-form natural language to document arguments and evidence, despite having a well-structured graphical outlook. As the complexity of the system being considered increases, assurance cases become excessively large and complex. In current practice, authors and evaluators manually review the entire case to ensure semantic correctness (the top-level claim logically follows from its sub-claims, arguments, and evidence), and that there are no logical inconsistencies or fallacies. Unfortunately, this process is timeconsuming and intellectually demanding, due to the inherent ambiguity, and inconsistency of natural language. Consequently, automating semantic reasoning would greatly reduce human efort and enhance the quality and confidence in these cases. However, free-form natural language is not conducive to such automation. Conversely, fully formal notations are impractical to represent assurance arguments.
To that end, we define a balanced approach that presents details in an intuitive and "minimally" formal way. We take a two-step approach, where we first categorically ground the terms used in the descriptions. Then the assurance case is transformed into a logical notation that can be subject to various formal analyses at the back end.
Fundamentally, assurance cases consist of blocks or "nodes" that describe the properties or relationships applicable to objects in a certain environment. Leveraging this general structure of description, we independently define the "Properties," "Objects," and "Environment" for each node, allowing us to formally express statements like "Object O satisfies property P in environment E." For instance, the assertion "Tim is a safe driver in the US" can be deconstructed into "Object = Tim," "Property = safe driver," and "Environment = US." When multiple objects and properties are associated with a node, it becomes necessary to specify their relationships, such as each property is applicable to all objects or each object or a specific object. This relationship is preserved and meticulously converted into appropriate logic predicates.
Currently, our ASCE assurance case authoring tool enables users to explicitly define objects, properties, and environments, along with their relationships to the assurance nodes, in addition to providing natural language descriptions. While the tool currently supports this dual specification, we are actively exploring methods to automatically extract Objects-PropertiesEnvironment information from the descriptions, thereby streamlining the process.
In order to convert the assurance case into a logical notation suitable for the desired semantic analysis, we opt for the domain of Logical Programming (LP). This choice is based on the fact that each concept in Assurance 2.0 and the intended analysis can be readily mapped to corresponding concepts in LP. The mapping between these concepts is illustrated in Table 1.
Assurance 2.0 Concept Top-level Claim Sub-Claims and Side-Claims Argument Evidence Defeater Binding Reasoning
Mapping to LP In the assurance case, the top-level claim aligns with the concept of queries in LP, which can be subjected to logical entailment analysis.
Sub-claims and side claims are analogous to predicates in LP serving the purpose of capturing the relationships between objects.
Arguments that establish relationships among sets of objects-propertiesenvironment can be equated to rules in LP where logical implications are utilized to describe these relationships.
Evidence artifacts that establish the truth about the system are facts in LP Defeaters are counter-claims to provide support for not believing that claim, which is the same as negation in formal logic theory definitions require the specification of variables for objects and the environment, that will be subsequently instantiated with terms when applied to a specific assurance case. This process aligns with the concept of substitution in LP, which involves dynamically mapping variables to terms.
Assurance case reasoning revolves around demonstrating that a top-level claim is entailed based on its arguments and evidence. This directly corresponds to proofs in logic, where the validity or truth of a claim is through logical reasoning.
By utilizing the Objects-Properties-Environment specification provided in each assurance case node, and based on the above concept mapping, the ASCE tool automatically translates the case into predicates in Prolog, a widely used logical programming language. The transformation process follows the guidelines presented in Table 2. In this table, the term ’ClaimPredicate’ refers to a Prolog predicate represented as the claim([O], [P], [E]), where [O], [P], and [E] represent comma-separated lists of Objects, Properties, and Environments associated with each assurance node. As we formalize the properties, the object-property relationships specified during the definition of objects and properties are preserved. This preservation ensures precision in the analysis. Consequently, the ’PropertyList’ is derived from the ClaimPredicate based on the specified object-property relationship, as enumerated in Figure 3. Furthermore, to maintain the structure of the case during export and ensure traceability, certain metadata (such as node identifiers, descriptions, etc.) is also included within the exported predicates.
Node Claim Evidence Side Claim Defeater
Prolog Translation claimStmt(‘Claim_ID’, Application, ClaimPredicate, ‘Description’) :[claimStmt|evidenceStmt|side_ClaimStmt], ClaimPredicate, theory (‘Theory_ID’,
Application, Claim). theory (‘Theory_ID’, Application, Claim). evidenceStmt(‘Evidence_ID’, Application, ClaimPredicate, ‘Artefact’, ‘URI’) :
ClaimPredicate.
ClaimPredicate :- PropertyList. side_ClaimStmt(‘Side_Claim_ID’, Application, ClaimPredicate, ‘Justification’) :
[claimStmt|evidenceStmt|side_ClaimStmt], ClaimPredicate.
ClaimPredicate :- PropertyList. false :- defeater(‘Defeater_ID’, defeats(‘Node_ID’), [O],[P],[E]).
defeater(‘Defeater_ID’, defeats(‘Node_ID’), [O],[P],[E]) :- PropertyList.
When ASCE tool exports the assurance case as Prolog predicates, to methodize the analysis, they are categorically saved in separate files: (i) the top-level claim is saved as a query, (ii) the negation of the top-level claim is saved as a negative query, (iii) the body of the assurance case – arguments, sub-claims, side-claims, and evidence – are saved together as rules and facts, (iv) theory definitions are saved separately, while their reference to applications are saved along with the body of the assurance case, and (v) defeaters are saved as integrity constraints that counter the claims. In the following section, we elaborate on various formal analyses.
The fundamental reason to translate the assurance case into Prolog predicates is to allow semantic analysis, which is otherwise not possible. In particular, our interest is to rigorously analyze the assurance case for the various properties that include but are limited to the following: • Indefeasibly Justified : Possession of adequate arguments and evidence that logically entails the top-level claim, and no unresolved defeaters remain. • Theory Application Correctness: Guarantee of correctness of application of theories • Property-Object-Environment Definition Consistency : Absence of contradictions in the property-object-environment definitions. • Evidence Validity and Adequacy: Existence and appropriateness of all evidence to support their respective claim • Completeness: Completeness with respect to the assurance case covering the domain of objects, properties, and environments defined for the system in consideration • Harmonious Coexistence of Theories: Ability among theories (definitions and their applications) to coexists within the same assurance case without causing logical violations.
In order to perform the aforementioned analysis of Prolog predicates, we leverage the
capabilities of s(CASP), a logic programming solver. Our choice of s(CASP) is based on several
reasons. Firstly, s(CASP) supports automated commonsense reasoning, which enables inferences
to be drawn from a set of predicates or knowledge in a manner similar to human reasoning.
This feature is particularly well-suited for reasoning about assurance cases. Moreover, s(CASP)
facilitates deductive and abductive reasoning, which is essential for proving whether a top-level
claim can be deduced based on the arguments, evidence, and assumptions in assurance cases.
Also, s(CASP) supports reasoning about global constraints and invariants, making it capable of
analyzing scenarios that violate these constraints. Additionally, the top-down solving strategy
employed by s(CASP) generates concise, human-understandable justifications [
In essence, using s(CASP), the verification of the correctness of the assurance case involves executing the query along with the body of the assurance case and defeaters. A successful execution results in the display of a “model," which essentially is a detailed explanation as to why the top-level claim is entailed. Conversely, if the query fails, no model is returned. In such cases, executing the negated query allows retrieving an explanation for the cause of the failure and its specific location. The returned model is presented in a tree structure, facilitating the understanding of the trace of what was entailed or failed. Failures typically occur due to the violation of one or more of the analyzed properties listed below.
This semantic property is fundamental to an assurance case. Possessing this property implies: (a) The top-level claim is suficiently supported by well-founded arguments and evidence, ensuring justification. (b) There are no unresolved defeaters that could potentially alter the decision regarding the top-level claim, called indefeasibility. When the positive query is successfully executed in s(CASP) and an explanation is provided, it signifies that the assurance case indeed possesses this property. Conversely, if the negative query is successfully executed, s(CASP) returns the unresolved defeaters as global integrity violations. An example output illustrating this scenario, for the safe driver example where claim node "C8" is defeated, is shown in Figure 4.
As previously explained, a theory consists of properties that are applicable to specific types of objects and environments. In theory nodes, objects, and environments are represented as Prolog variables (names starting with an uppercase letter). During the authoring of assurance cases, "types" of objects and environments, as well as all possible instantiations (constants defined with lowercase letters) are all pre-defined. The author appropriately selects them during theory definition and application. To ensure that incorrect instantiations are avoided, we utilize s(CASP). The analysis involving theories is more complex compared to others since s(CASP) dynamically associates the variables in theories with the constants in theory application.
When utilizing theories in the analysis process with s(CASP), it involves verifying the correctness of theory application based on two key factors: (a) Ensuring that the constants chosen as objects and environments align with the respective instantiations defined in the theory. (b) Validating that the properties specified in the theory nodes correspond to the properties in the corresponding application nodes. For instance, let’s consider the scenario depicted in the "Theory of Safe Driver" definition and its application in Figure 2. A correct application of this theory will yield a comprehensive justification tree, exemplified in Figure 5. However, if there were any inaccuracies in specifying the properties or objects, executing the negated query will result in a justification that can be used to trace the error and identify the issue at hand.
Inconsistencies within the specifications of properties, objects, and environments in the nodes of an assurance case can pose a problem as they may lead to flawed validation of assurance arguments. While logical solvers can easily identify conflicts between predicates and their negations in logical representations, conflicts based on natural language words are not as straightforward to detect. For example, in natural language, words like ‘good driver’ and ‘bad driver’ are considered opposites, but in logic, they may not be. However, from an assurance case perspective, it is crucial to semantically identify and report such opposites and conflicts. To address this issue, we propose the introduction of specialized, domain-specific rules. For instance, in the safe driver assurance case, conflicts among property specifications such as ‘good driving habits’ for Tim in one node, and ‘bad driving habits’ for Tim in another, can be detected and reported by s(CASP) by incorporating a rule that ‘bad driving habits’ for any person is the negation of ’good driving habits’ for that person.
The provision of appropriate evidence is crucial to assurance cases. While ASCE tool structurally detects claims with missing evidence nodes, incorrect or inadequate evidence within the evidence node is essentially a semantic check. By introducing domain-specific rules relevant to evidence will help automatically detect and report the issues. For instance, by introducing a rule that requires testimonials of ‘good driving habit’ by two or more safe drivers (E1 node in Figure 1), s(CASP) can report inadequacies in the provided evidence. Since s(CASP) can perform substitution, these rules can be defined using Prolog variables and reused for other assurance cases in the domain. We are currently investigating generic rules that can be broadly applied to a class of evidence. For instance, test-case artifacts should also always have an associated coverage analysis report.
In general, completeness is the state of encompassing everything that is needed. Given a predefined global set of objects-properties-environment for the system in consideration, and by defining a rule such as ‘domain completeness’ that requires every property-object-environment is used at least once in a claim or evidence node, we can leverage s(CASP) to analyze the completeness of assurance case. For instance, in the safe driver case, if there are multiple types of vehicle inspection records available in the domain, while Tim’s case only accounts for one of them, s(CASP) can help report the incompleteness; this can either be resolved by adding the evidence to the case or removing the additional one from the domain.
Completeness refers to the state of encompassing all the necessary elements. To assess the completeness of an assurance case, we can utilize the pre-defined global set of objects, properties, and environments for the system under consideration. By defining say, a "domain completeness" rule that required every property-object-environment combination to be used at least once in a claim or evidence node, and employing s(CASP) for analysis, we can evaluate the completeness of the assurance case. For example, in the case of safe driver assurance, if there are multiple types of vehicle inspection records available in the domain, but Tim’s case only included one of them, s(CASP) can be leveraged to precisely identify the incompleteness.
Theories are reusable assurance fragments that can be independently specified, and ‘pre-certified’ and be applied to diferent cases. when constructing assurance cases, more than one theory may be applied to an assurance case. However, when multiple theories are linked and applied within an assurance case, there is a risk of conflicting properties among their definitions or in their concrete applications. We are currently exploring approaches to define novel rules and will allow s(CASP) to check for the presence of conflicts, or determine that the theories can harmoniously coexist within that assurance case.
The realm of semantic analysis ofers a wide range of possible analyses. As part of our ongoing work, we are exploring valuable and powerful properties to analyze. Automating these analyses will provide valuable insights and relieve humans from repetitive tasks, leading to improved decision-making regarding assurance cases.
Our Assurance 2.0 framework is designed to facilitate reasoning and communication regarding the behavior and trustworthiness of engineered systems, with the ultimate goal of achieving certification. In this paper, we have presented our approach to augment it with semantic analysis capabilities. We begin by systematically converting the Assurance 2.0 case into Prolog predicates and utilize s(CASP) to conduct various semantic analyses. We have conducted evaluations on complex systems, and the preliminary results show promise. As a result, we are further enhancing the capabilities of our tools and techniques to enable more in-depth analysis of the semantics of assurance cases.
This work is supported by DARPA Automated Rapid Certification Of Software (ARCOS) program under agreement number FA875020C0512 for Consistent Logical Automated Reasoning for Integrated System Software Assurance (CLARISSA) project. The views, opinions, and/or findings expressed are those of the authors and should not be interpreted as representing the oficial views or policies of the Department of Defense or the U.S. Government.