ExplicitCase - An Assurance Case Editor in AF3

AutoFOCUS3 contains an editor, named ExplicitCase, which supports the construction of modular assurance cases, in compliance with the Goal Structuring Notation (GSN) standard.

Support for Assurance Case Creation

Assurance cases constitute a proven technique to systematically demonstrate the safety/security/reliability of such systems using existing information about the system, its environment and development context, facilitating the bridging of the regulatory gap. Three parts can be identified as part of an assurance case. First, the goal that has to be achieved. Second, the evidence for achieving this goal and third, the structured argument constituting the systematic relationship between the goal the evidence. Assurance cases can be designed in a modular approach, by subdividing complex assurance cases into interconnected modules of assurance arguments and evidence.

What is the Goal Structuring Notation (GSN)? Why shall assurance cases be satisfied via this notation?

The Goal Structuring Notation (GSN) is a well-known description technique for the development of engineering arguments to construct assurance cases. GSN uses a graphical argument notation to explicitly document the elements and structure of an argument and the argument's relationship of this evidence. An argument, based on GSN, may consists of several elements: Goals are the claims of an argument, whereas items of evidences are captured under Solutions. When documenting how claims are said to be supported by sub-claims, the Strategy-element is used and can be linked to Goals. A Context element captures and enables citation of information that is relevant to the argument. Rationale for a strategy can be described by a Justification element. GSN provides two types of linkage between elements: SupportedBy and InContextOf. SupportedBy relationships indicate inferential or evidential relationships between elements. InContextOf relationships declare contextual relationships. The benefit of having a structured graphical notation for assurance cases is that it supports the presentation of assurance cases to non-safety experts in a comprehensive manner.

GSN-based assurance cases in AF3

ExplictCase is based on a metamodel derived from the GSN standard and offers a graphical editor facilitating the model-based development of assurance cases. An overview of the editor is shown in Fig. 1. The editor provides complies with the GSN standard, by allowing the user to build assurance cases via:

Steps to create an assurance case for your project

  1. Go to an AF3 project, in the Model Navigator view and right-click on it;
  2. Select the Assurance Argumentation Package item from the context menu;
  3. Go to the newly created Assurance Argumentation Package, in the Model Navigator view, and right-click on it;
  4. Select the Assurance Case item from the context menu;
  5. Go to the newly created Assurance Case, in the Model Navigator view, and double-click on it, so that the editor (a Modeling Diagram) in which you can model the assurance case appears.

Steps to add argumentation nodes

  1. Go to one of your assurance case modules from the Model Elements view and double-click on it, so that the editor (a Modeling Diagram) in which you can model the assurance case module appears;
  2. To add an Argumentation Node, drag and drop a Goal/Away Goal /Strategy/Solution/Away Solution/Optional Entity/Strategy /Justification/Assumption/Context/Away Context from the Model Elements view on the right side to your diagram; Note: To move an argumentation node, just pick the module somewhere in the middle and move. To resize it, pick it in the lower right corner and move the mouse to resize.
  3. In order to create relationships between your argumentation nodes, namely SupportedBy and InContextOf relationships, as specified in the GSN standard, press the alt-Key (ctrl-Key under Linux) on your keyboard and drag the relationship from one argument element to another. Invalid relationships (e.g., between a solution and a context) are avoided by disabling the dragging.

Setting properties of assurance argumentation nodes

Properties of assurance argumentation nodes can be set in the Properties view. There are two types of properties, namely general properties, which may be set to all types of GSN nodes and specific properties, which may be set only to particular types of GSN nodes. The following properties are properties to be set to any type of GSN node:

  1. Name of the GSN node in the Name text box;
  2. Comment regarding the GSN node in the Comment text box;
  3. ID of the argumentation node in the Element identifier text box;
  4. Claim of the GSN node in the Comment text box. This text may and should be filled in for all types of GSN nodes, except for solution nodes. Furthermore, you cannot set claims to away entities, as they have the same claim as the assurance argument element the point to.;
  5. Add a reference to a document to the GSN node by pressing the Add document button. A file browser will open and you can select any file of type pdf/Word/Excel;
  6. To delete a reference, press the Remove document button;
  7. To give some further explanation of the reference to a certain document, use the Reference Explanation text box;

Setting properties of SupportedBy and InContextOf relationships

  1. As you create an assurance case pattern, you can assign a multiplicity to a relationship, by writing any number higher than 0 in the Multiplicity text box. You can give a short explanation of the multiplicity in the corresponding text box;
  2. Mark the relationship as Optional, by checking the corresponding check button.
  3. For SupportedBy relationships, set the relevance, support and strength levels of your relationships by selecting from the drop-down lists.

Setting properties of Option Entities

  1. You can select the assurance argument elements you want to keep for your assurance argumentation structure, by right-clicking on the option entity node, and selecting the Make a choice context menu element. A wizard will appear in order to select from the optional elements.
  2. You can write down in the The minimum required text box from the Properties view, the minimum number of assurance argument elements that should be selected to be kept in your assurance argumentation structure.

Setting particular properties of Goals

  1. Scope a goal to a particular AF3 logical component by pressing the Add scope button;
  2. Remove the scope of a goal to a particular AF3 logical component by pressing the Delete scope button;

Setting particular properties of Away Entities

Right-click on the away entity. A context menu will appear. Click on the Connect 2 Goal/Solution/Context menu item A wizard will appear. Select from the assurance argument nodes that appear in the wizard, one to which you want your away entity to point to. If the selected node was set as private, you will be asked if you want to change the visibility of the node. If not, the reference will not be done. Only public nodes may be referenced by away entities. In the Properties view, in the Referenced module ID the ID of the module containing the node referenced by the away entity node is automatically filled in.

Setting states to GSN nodes

According to the GSN standard, a node may take different states in the course of the assurance case development. One may right-click on a GSN node and select the following states: private/public, instantiated/uninstantiated, developed/undeveloped and supported by contact.

Tool-based Support for Handling Large Arguments

What are modular assurance cases? Why shall assurance cases be modular?

One way of designing assurance cases is by following the modular approach. In GSN, an assurance case module contains the objectives, evidence, argument and context associated with one aspect of the assurance case. In addition to the GSN argument elements presented in the previous paragraph, a module may contain away entities such as away goals, away solutions and away context elements. Away entities are references to the goal, solution or context in another module. Away goals cannot be (hierarchically) decomposed and further supported by sub-entities within the current module; rather, decomposition needs to occur within the referenced module. Inter-modular relationships are of two types: namely supported by and in context of relationships. A supported by relationship denotes that support for the claim presented by the away goal or away solution in one module is intended to be provided from an argument in another module. When there is an away context element in a module, that module is connected to another module by an in context of relationship; relationship that indicates that the context of a certain claim will be presented in details in another module.

Modularity of assurance cases has various advantages, namely:

Modular assurance cases in AutoFOCUS3

ExplicitCase enables the user to model an assurance case containing several modules which are connected to each other through intra-module connections (see Fig. 4). Each such module contains an assurance argumentation structure, build up by GSN-defined elements specific to modularity in assurance cases (i.e., Away Goals, Optional Entities, Away Solutions, Away Contexts, Contracts) connected to each other by GSN-defined relationships. Each argumentation node within a module has a public indicator, which determines whether the element may be referenced in another module, or not.

Fig. 4 - Assurance case modules.

Steps to create an assurance case module

  1. After creating your assurance case, you can now specify the contained assurance case modules. To add an assurance case module (called Argument Module in AF3), drag and drop an Argument Module from the Model Elements view on the right side to your diagram; Note: To move a module, just pick the module somewhere in the middle and move. To re-size it, pick it in the lower right corner and move the mouse to re-size.
  2. To specify properties of the module, go to the Properties view. There you can assign the assurance case module an id (in the Element Identifier text box). All other text box may not be filled in;
  3. To generate intra-module connections, based on the away entities, go to your assurance case, in the Model Elements view and right-click on it. Select the Generate Module Connections item from the context menu. Do consider that, if you do not have any away entities in your assurance case modules, you will not have any relationship between your modules.


Steps to specify the contained elements of an assurance case module

Once you are done with specifying the modules of your assurance case, you can describe the assurance argument structure contained by these modules by adding argumentation nodes.

Here is an example of the assurance argumentation structure an assurance case module modeled in AF3:

Visual aids

Different coloring of GSN elements raises the assurance case developer's awareness about the existence of undeveloped or uninstantiated entities (see Fig. 5). In addition, contract modules have a distinct coloring in order to distinguish them from regular argumentation modules. We do not allow users to color nodes by themselves, in order to keep a certain meaning of each coloring so that anyone can easily "read" the coloring. This is motivated, by the fact that the GSN Standard says that, In cases where the elements defined in these sections are used in the development of instantiations of the patterns to produce individual assurance arguments, it is important to ensure that they are all removed, or instantiated, in the final, delivered, version of the argument.

Fig. 5 - Different coloring for different node properties.