ExplicitCase - A Safety Case Editor in AF3

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

Feature 1: Safety Case Editing.

Safety cases constitute a proven technique to systematically demonstrate the safety 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 a safety case. First, the safety goal that has to be achieved. Second, the evidence for achieving this safety goal and third, the structured argument constituting the systematic relationship between the goal the evidence. Safety cases can be designed in a modular approach, by subdividing complex safety cases into interconnected modules of safety arguments and evidence.

What is the Goal Structuring Notation (GSN)? Why shall safety 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 safety 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 safety cases is that it supports the presentation of safety cases to non-safety experts in a comprehensive manner.

GSN-based safety 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 safety 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 safety cases via:

Fig. 1 - GSN compliance.

Feature 2: Hyperlinking

There are several types of hyperlinking offered by ExplicitCase. First, we distinguish between hyperlinking words in safety claims and linking an entire GSN node to another artifact. Second, hyperlinks can link the safety case with external documents containing safety reports, safety analysis or verification results or even system models (see Fig. 2). AF3 provides the "native" internal system models that may be linked to elements of safety cases modeled in ExplicitCase. The novelty of our hyperlinking system lays in the fact that words in claims or GSN nodes are deeply integrated with the system artifacts created by the user in the AF3 model-based development tool. The user may link words in claims, or entire GSN nodes to AF3 artifacts from different phases of the safety process (e.g., requirement and deployment models), as well as implementation (e.g., generated code), and verification artifacts (e.g., simulation, formal verification or testing results).

Fig. 2 - Linking GSN nodes with AF3 and external artifacts.

Feature 3: Reference to external documents

Since the most common approach for describing safety cases in the industry is free text, the user can add to any modeled GSN node a reference to the document in which further explanation of the claim in the node may be found. Furthermore, the user can add a string, which depicts a reference to the paragraph from the referenced document in which the node is explained in detail (see Fig. 3). This feature is motivated by the fact that pure graphical notation can demonstrate links between argument sections and differentiate between different types of argument components, but without narrative there is no "meat" against which the soundness of the argument may be judged.

Fig. 3 - Reference to an external document.

Feature 4: Tool-based Support for Handling Large Arguments

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

One way of designing safety cases is by following the modular approach. In GSN, a safety case module contains the objectives, evidence, argument and context associated with one aspect of the safety 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 safety cases has various advantages, namely:

Modular safety cases in AutoFOCUS3

ExplicitCase enables the user to model a safety case containing several modules which are connected to each other through intra-module connections (see Fig. 4). Each such module contains a safety argumentation structure, build up by GSN-defined elements specific to modularity in safety 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 - Safety case modules.

Feature 5: Visual aids

Different coloring of GSN elements raises the safety 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.

Feature 6: Built-in Safety Case Model Constraints.

Model constraints define semantic conditions that cannot be defined in the syntactic structure of a metamodel. Since different stakeholders may have different interpretations and the underlying assumptions may be overlooked, ExplicitCase requires to document goal decompositions via strategies. Therefore, a constraint on the safety case model enforces the existence of a strategy node whenever the user wants to connect two goals. ExplicitCase checks many more constraints to ensure the integrity of safety cases (e.g., to prevent the creation of invalid relationships). For example, another constraint to ensure the integrity of safety cases is that only GSN connections permitted by the GSN standard can be modeled (e.g., a context node cannot be connected to a justification node). Avoidance of circular argumentation is another built-in constraint on the semantic level.

Feature 7: Status Notifications

ExplicitCase offers on-the-fly checks of arbitrary complexity. We define two types of notifications: warnings and errors. Errors signal missing or erroneous information, whereas warnings indicate safety case nodes that need to be given further consideration. The type of notifications to be get may be manually selected by the user. For example, an error is signaled when a goal is changed and the supporting solution should be reconsider (see Fig. 6). Warnings are, for instance, raised for option entities that cannot be left in the final version of the safety case, but must be appropriately resolved (see Fig. 7).

Fig. 6 - Error reports in ExplicitCase.
Fig. 7 - Warning reports in ExplicitCase.

Feature 8: Maintenance

Throughout the operational life of any system, changing regulatory requirements, additional safety evidence and a changing design can challenge the corresponding safety case. In order to maintain an accurate account of the safety of the system, all such challenges must be assessed for their impact on the original safety argument.

Why do we need maintenance?

A safety case consists of many inter-dependent parts: safety requirements, argument, evidence, design and process information. As a result, a single change to a safety case may necessitate many other consequential changes - creating a 'ripple effect'. It is significant to recognize the importance of every challenge to a safety case. Furthermore, the indirect impact is crucial and one of the biggest challenges. Any of these challenges imply re-certification and by extension re-generation of the safety case of a system. The construction and maintenance of safety case arguments is expensive and tedious, as it is mainly a manual process that requires a considerable amount of time. Therefore, offering safety engineers tool-supported re-evaluation is a big step forward.

What is the algorithm for maintenance?

The maintenance algorithm includes the handling of challenges regarding the following different argument elements.

Potential vs. actual change effect

The rules described above constitute the potential change effect and not necessarily the actual change. There is a significant difference between actual and potential change. The nodes to which the impact of the challenge in a connected GSN node propagates are called impacted nodes. The potential change includes further analysis of the possible effects on the rest of GSN nodes after one element is challenged. A safety engineer has to review all the potential challenges and decide upon them. ExplicitCase implements as a starting point, the potential change effect.

Safety Case maintenance in ExplicitCase

The safety case maintenance in ExplicitCase requires the participation of different entities and stakeholders (see Fig. 8). The system modeling is done by the system engineer and the GSN modeling of the safety cases by the safety engineer. The safety engineer has also responsibilities such as hyperlinking GSN with System Models and annotating GSN safety cases with maintainability information. ExplicitCase recognizes challenges to validity of GSN safety cases and identifies the impact of a GSN node challenge. Finally, the safety engineer gives input to the system engineer regarding the reasons why, after a change in one system model element, other system model elements, should be reviewed.

Fig. 8 - Stakeholders in ExplicitCase.

Steps to maintenance in ExplicitCase

  1. Follow the steps in the section "Steps to specify the contained elements of a safety case module" and build a safety case module;
  2. Select the Solution Argument Element and right-click on it. Click 'Is Challenged';
  3. The challenged solution has changed its color to red;
  4. Right-click again on the challenged solution. Click 'Show potential change impact';
  5. The potentially impacted argument elements, by the challenged solution, have turned their color to yellow;

Deprecated: Safety Case Patterns

Apart from the aforementioned features, ExplicitCase enables its user to create safety case patterns store them in an AF3 library. However, this feature is currently under construction.

Steps to create a safety case for your project

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

Steps to create a safety case module

  1. After creating your safety case, you can now specify the contained safety case modules. To add a safety 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 safety 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 safety 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 safety case modules, you will not have any relationship between your modules.

 

Steps to specify the contained elements of a safety case module

Once you are done with specifying the modules of your safety case, you can describe the safety argument structure contained by these modules as such:

  1. Go to one of your safety 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 safety 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.

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

Setting properties of safety argumentation nodes

Properties of safety 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 safety 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 a safety 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 safety argument elements you want to keep for your safety 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 safety argument elements that should be selected to be kept in your safety 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 safety 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 safety 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.

Hyperlinking Goal nodes

Connect a goal to a modeled safety requirement from the Requirements Analysis of the project, by right-click on the goal node, and pressing the Connect 2 Requirement element from the context menu that will appear after right-clicking. When connecting a goal to a safety requirement, the name and the claim of the goal will be the same as the name and the description of the requirement. To go directly to the requirement referenced by the goal, go to your goal in the Model Elements view, right-click on it and select the Go To Referenced AF3 Element menu item. If you want to delete the reference, just right-click on the node, and select the Eliminate Reference context menu element.

Hyperlinking Solution nodes

Connect a solution to an already modeled AF3 element, by right-click on the solution node, and pressing either the Connect 2 Platform (for referencing to an AF3 element of type platform), the Reference Test Coverage (for referencing to an AF3 element of type result constraint), the Reference Test Results (for referencing to an AF3 element of type coverage constraint), or the Connect 2 Generated Code (for referencing to files containg AF3 generated code) elements from the context menu that will appear after right-clicking. When selecting the test results or test coverage as evidence for the solution, the results, or, respectively, the coverage, of the test suite, referenced by the context of the goal supported by the solution are regarder. If no test suite is refered by the context of the goal node, a notification is raised. When connecting a solution to an AF3 element, the name of the solution will be the same as the name AF3 element. To go directly to the element referenced by the solution, go to your solution in the Model Elements view, right-click on it and select the Go To Referenced AF3 Element menu item. If you want to delete the reference, just right-click on the node, and select the Eliminate Reference context menu element.

Hyperlinking Context nodes

Connect a context node to Test Suite of a certain logical component in the project, by right-click on the context node, and pressing the Connect 2 Test Suite element from the context menu that will appear after right-clicking. Only test suites of the component that is scoped by goal node to which the context node is associated the my be selected. To go directly to the test suite referenced by the context, go to your goal in the Model Elements view, right-click on it and select the Go To Referenced AF3 Element menu item. If you want to delete the connection, just right-click on the node, and select the Eliminate Reference context menu element.

Hyperlinking Assumption nodes

Connect an assumption node to a State or Mode of the component scoped by the goal node for which the assumption node was created, by right-click on the assumption node, and pressing the Connect 2 State or Connect 2 Mode element from the context menu that will appear after right-clicking. To go directly to the requirement referenced by the assumption node, go to your goal in the Model Elements view, right-click on it and select the Go To Referenced AF3 Element menu item. If you want to delete the connection, just right-click on the node, and select the Eliminate Reference context menu element.

Deprecated: Safety Case Patterns in AF3

Steps to create a safety case pattern in AF3

  1. Create a new safety case module;
  2. Specify the safety argumentation structure of this module;
  3. Make sure that all the safety argument elements contained by your module are marked as uninstantiated entities.

When you are done with modeling your pattern, do the following steps:

  1. Go to the File on the menu bar and click on it;
  2. Select New AF3 Library from the drop-down menu;
  3. Go to the Model Navigator view and select the Toggle library view button;
  4. Select the newly created AF3 Library from the Model Navigator view and right-click on it;
  5. Select New Package (for safety argument patterns) from the drop-down menu;
  6. Go to the Model Navigator view and deselect the Toggle library view button;
  7. When you are done with the modeling of the safety argumentation pattern, go to the newly created Argument Module from the Model Navigator view and right-click on it;
  8. Then select Add to Library from the drop-down menu;
  9. From the opened dialog, select the newly created safety argument patterns package.

Steps to apply a pattern into your safety case

  1. Go to your Safety Case in the Model Navigator view and double-click on it. This will open your safety case in the Modeling Diagram view;
  2. Apply the pattern you created to your safety case by drag-and-drop from the Model Elements view.

Note: All the available safety case patterns in your workspace are to be found under Library -> safety argument patterns in the Model Elements view.

Instantiate a safety case pattern

  1. Go to the newly imported Argument Module from the Model Navigator view and right-click on it;
  2. Select Disconnect from library item from the context menu;
  3. Go to the Safety Argument Properties view for each of the elements of the module and do the following steps:
    1. Fill in the Element Identifier text box;
    2. Replace the words in curly brackets from the claim of the safety argument element, by editing the claim or by pressing the Instantiate the words in curly brackets from the claim button;
    3. Deselect the Uninstatiated entity button.