Modularisation is helpful in managing large and complex assurance cases. It also allows to distribute responsibilities and manage access rights on the level of single modules. Modularisation is required to enable reuse of arguments.
NOR-STA implements modular argument metamodel defined in OMG SACM and extends it to implement three types of bindings between argument modules specified in GSN Community Standard.
Splitting an assurance case into modules enables presentation of its architecture using modular diagrams. You can develop separate argument modules for different system components or functions, hazards, threats, standards or other properties.
The breakdown of the argument into modules is usually made in claims. Any claim in the argument may be used as an interface between the modules. The support relation between argument modules presented in the diagram is in fact a support relation between connected claims. We will use GSN diagrams In this text. The direction of the arrow presents the relation ‘is supported by’.
The architecture diagram presents three argument modules. The top one describes mitigation for a hazard. The two others provide the argument how two components support the hazard mitigation. Each module can be developed by an independent team.
The connection points between the modules are claims. This will be presented in the next diagram. The two claims in the top argument with the module icon and a name of the supporting module are called ‘away elements’ according to the GSN terminology. They are links to the corresponding claims in the supporting modules.
Connecting modules may look simple but the implemented formal model is quite complex. First we should distinguish two roles of connected claims. Some of them require to be supported while the others provide support. The two claims in the top module require support. The top claims of two modules SENSOR and VALVE provide support.
The next step is to group these claims in the interfaces. An interface is a container of argument elements (claims) made available for other argument modules for connection. There are two main types of interfaces:
- Required interfaces contain unsupported claims which require to be supported by claims in other argument modules.
- Provided interfaces contain claims which can provide support for other argument modules.
It is not allowed to mix required claims and provided claims in one interface in NOR-STA. Separate interfaces should be used for claims which require to be supported and for claims which provide support.
When we have claims in the interfaces we can connect then with a binding. A binding is a connection which works on two levels:
- Interface binding connects a required interface in one module with a provided interface in another argument module.
- Element binding connects two elements (claims) in the interfaces, where one requires to be supported and another one provides the support.
GSN diagrams do not show the interfaces. GSN standard defines a concept of a module interface (1:4.6) as a collection of all required and provided elements together. NOR-STA implements a more advanced concept of interfaces as defined in OMG SACM. This allows creation of more than one interface ahich can be provided for different audiences. We will extend the GSN diagram to present the interfaces and bindings. Note that we have also added a new interface with the claim G0 to present that we use separate required interfaces and separate provide interfaces. The difference between NOR-STA and the GSN standard is that the GSN standard defines one interface to contain all required and public elements and in NOR-STA there are separate interfaces.
An interface can include more then one element of the argument. You can create any number of interfaces. Managing the interfaces and bindings may seem to be complex task but in practice you can often ignore them. NOR-STA can create the interfaces automatically when necessary.
The connection between claims presented in the diagrams above is of a type called ‘away element’. There are three types of connections defined in GSN and implemented in NOR-STA.
Away element – a citation of an element in another module will be created in your argument. This is simply a link to a claim in the supporting module. You will not be able to edit the name nor the description of an away element as they are taken directly for another module. If the module symbol is empty it means that there is no binding and that the element waits to be linked to the supporting module
Supported by another module – the element in your argument is supported by another element in a supporting module. This type of connection is represented by a module icon decorator below the element. When the element is supported by another module then its symbol is printed next to the module icon.
Supported by a contract – the binding is automatically extended with a dedicated step of reasoning called a contract. The contract says that the supporting claim is sufficient to justify the supported claim in its full context. The objective of the use of contracts if to force the user to review every binding.
The distinction of three types of bindings between argument modules is compliant with GSN Community Standard. Please refer to Modular Extension in GSN Standards for more information about the types of bindings.
The type of the binding is to be chosen by the NOR-STA user at the time when the required interface is created. The provided interface can accept any type of the binding.
How to choose the type of the binding for the required interface?
- If you need a link to a claim in another module please select away element. The name and the description from the source argument will be presented. When the provided claim is modified you will automatically see its current name and description.
- If you need to connect two claims you should choose the option supported by another module. The binding of this type creates an ‘is supported’ relation between two claims in different argument modules. This is the simplest way to connect two claims.
- Choose the last option (supported by a contract) when you need verification of the binding. A simple contract argument will be created automatically for each binding and it can be available for the assessment. Each binding will need individual review and conformation by the user that it is valid.
There are many topics not covered in this short text, for example how to manage context in modular arguments and how to make sure that the context of a supporting modules fits.
To learn more about modular assurance cases in NOR-STA refer to NOR-STA manual or join our online training on the 18th of May.