AutoFOCUS3 contains an editor, named ExplicitCase, which supports the construction of modular assurance cases, in compliance with the Goal Structuring Notation (GSN) standard.
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.
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.
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 allows the user to build assurance cases via GSN, as follows:
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 goals, solutions or context elements 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:
ExplicitCase enables the user to model an assurance case containing several modules which are connected to each other through intra-module connections. Each such module contains an assurance argumentation structure, build up by GSN-defined elements specific to modularity in assurance cases (i.e., Away Goals, 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.
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 elements.
Properties of assurance argumentation elements 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 elements and specific properties, which may be set only to particular types of GSN elements. The following properties can be set to any type of GSN node:
Away entities act as interface of argument modules. An away entity references an argument element in another module. Right-click on the away entity in the Model Navigator View. A Context Menu will appear. Click on the Connect to Goal/Solution/Context menu item and a wizard will appear. Select from the assurance argument elements 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 you do not that, the reference will not be done. Only public elements 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. After setting a reference to an entity, you can go again in the Model Navigator View and right-click on the away entity and select "Go To Refenced ..." button from the Context Menu.
According to the GSN standard, an argument element may take different states in the course of the assurance case development. One can right-click on a GSN element in the Model Navigator View and select the following states: private/public, instantiated/uninstantiated, developed/undeveloped and supported by contract.
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 elements 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.
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 assurance 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 assurance cases (e.g., to prevent the creation of invalid relationships). For example, another constraint to ensure the integrity of assurance 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.