COMPASTA: Integration of the TASTE and COMPASS toolsets

Introduction

COMPASS is a tool for model-based system/SW co-engineering developed in a series of ESA studies (2008-2016). It offers a complete set of functionality for formal verification, including requirements specification and analysis, contract-based design and verification, functional verification, fault specification, fault injection and RAMS analyses, including Fault Tree Analysis (FTA), Failure Modes and Effects Analysis (FMEA), Diagnosability Analysis, Fault Detection, Isolation and Recovery Analysis (FDIR). The COMPASS engines, providing formal verification capabilities, are based on model checking.

COMPASTA integrates the COMPASS functionality into TASTE, thus providing a comprehensive, end-to-end tool chain that covers system development, early verification and validation, safety assessment and FDIR, and system deployment.

In summary, the COMPASTA workflow can be described as follows:

• COMPASS is used to build and validate a formal model of the system (including both HW and SW) architecture, to specify the behavior of the HW components and their faults
• TASTE is used to model the behavior of the SW components, for deployment and code generation, and to test the final implementation

Specifications in COMPASTA are based on the AADL and SDL as specification languages AADL is used for the interface view and for the specification of the behavior of the HW components. SDL is used for the specification of the behavior of the SW components.

COMPASTA verification engines comprise:

• the nuXmv model checker [1]
• the xSAP safety anaysis platform [2]
• the ocra tool for contract-based design and refinement [3]

Further details on COMPASS can be found on the COMPASS web site [4] and in the COMPASS documentation page [5].

Installation

COMPASTA is integrated with TASTE and can be installed along with it. COMPASTA is currently available in the branch called "feature_bullseye" of the taste-setup [6] ESA repository. COMPASTA installation requires downloading this specific branch.

Available installation options are described in [7]'

COMPASTA Workflow

We illustrate the COMPASTA workflow on the following example of a redundant power system. In this example, generators are used to charge batteries, which in turn power sensors. The lines connecting generators, batteries and sensors are redundant, and can be re-configures in case of faults. HW component may be subject to the following faults: faulty generators and batteries do not provide power, faulty sensors do not provide valid outputs. Two FDIR components control system re-configuration in case of faults, acting on the corresponding switches they are connected to. The system is operational if sensors are powered and provide valid outputs.

To open the working example in the COMPASTA distribution, follow the steps below.

    $ source ~/.bashrc.taste 
    $ cd ~/tool-inst/share/compasta-code/examples/models/battery_sensor 
    $ taste 

The COMPASTA workflow is composed of the following steps.

Modeling the System Architecture

The system architecture is modeled using TASTE Interface View graphical editor. A new implementation language called "slim" is provided to specify the behavior of the HW components. COMPASTA supports SDL to specify the behavior of the SW components, and slim for the HW.

COMPASTA expects that the TASTE model contains a top-level block called "SystemBlock", containing a (flat) hierarchy of components (both HW and SW components).

HW-SW communication is realized via unprotected ports, whereas SW-SW communication may also use sporadic interfaces. SW components must have an input cyclic port. SW components are implemented in SDL, using OpenGEODE. HW components are implemented using the Slim language.

In COMPASTA, we need to model open systems (e.g., for contract-based analysis), i.e., systems with unconnected interfaces at the top-level. Since this is not supported in TASTE, COMPASTA requires "SystemBlock" to be connected to an additional component called "PROPS" which is used to connect the open interfaces from "SystemBlock".

Modeling the Behavior of HW Components

The behavior of a HW component is specified in slim. The slim language is defined in COMPASS and adapted in COMPASTA. Documentation can be found in [8].

The fragment of the language supported in COMPASTA is documented in the syntax and semantics document distributed with the tool.

First, we set the Slim language to a function block by right-clicking on the block and by selecting "Properties" from the contextual menu.

The "Properties" window appears. Slim can be set as implementation language in the tab "Implementations".

The behavior can be edited by selecting “Edit implementation” from the same contextual menu seen above. As a result, a syntax-highlighted SLIM file will be created and opened in Space Creator’s editor. An example specification is shown below.

If the file does not exist, a new file is created, containing a comment at the top with information about the function interfaces in the TASTE model along with a skeleton code.

Modeling the Behavior of SW Components

The behavior of a SW component is specified in SDL using the OpenGEODE editor. For SDL, see the Detailed SDL tutorial.

The behavior can be edited by selecting “Edit implementation” in the contextual menu. An example specification for the "FDIR_2" component is shown below.

The following SDL constructs are not (yet) supported by the COMPASTA translator:

• Array type
• Nested structures
• Nested states
• Parallel states
• Exported procedures

Modeling Faults, Properties, Contracts and Requirements

To model faults, from Space Creator’s menu bar, select "Tools → COMPASTA Tools → Edit Faults".

A syntax-highlighted slim file named fault.slim opens within Space Creator’s editor. This file contains fault injection specifications for all the HW components' blocks. An example is shown below.

If the file does not exist, a new file is created, containing a comment at the top with information about the function interfaces with a skeleton code.

A similar workflow applies to the specification of contracts, properties and requirements. Example specifications are shown below.

Contracts are specified using the slim syntax defined in COMPASS.

Properties are specified in slim, similarly to COMPASS. COMPASTA supports specification of generic properties, and specification via property patterns.

Requirements are specified with reference to existing properties.

Verification and Validation

In COMPASTA, fault specifications are automatically injected into the system model (called the nominal model). The resulting model is called extended model, since it is extended taking into account the fault specifications. The user can carry out verification and validation analyses either on the nominal or the extended model (some analyses, e.g. RAMS analyses, are carried out on the extended model by default, since they have to take into account the faults). The model(s) along with the specifications of properties, contracts and requirements are input to the verification and validation engines.

The verification GUI can be opened from TASTE’s menu bar: "Tools → COMPASTA Tools → Open Verification GUI".

The GUI gives access to the following tabs/sub-tabs which offer the corresponding verification methods:

• Requirements Analysis
• Contract-Based Analysis
  • Validation
  • Contract Refinement
  • Tightening
• Correctness
  • Property Verification
  • Contract Verification
• Safety
  • Fault Tree Analysis
  • Failure Modes and Effect Analysis (FMEA)
  • Hierarchical Fault Tree Generation
• FDIR
  • Fault Detection Analysis
  • Fault Isolation Analysis
  • Fault Recovery Analysis
  • Diagnosability Analysis

For each method, the user can select the desired parameters in a dedicated toolbar which is located at the top of the tab content. In the same tab, the user can select the formal specifications to be verified (e.g., properties). The specifications are located immediately below the toolbar. Once the specifications are selected, the user can click on the button "Run" located on the left-hand side of the toolbar. As a result, the verification task is started.

Below we show two examples (Property Verification and Fault Tree Analysis).

Property Verification

The Correctness → Property Verification contains three main sections: toolbar, "Property List" and "Fault List".

The first row of the toolbar contains two buttons: "Run PV" on the left, and "Help" on the right. "Run PV" will start the verification process, while "Help" shows the following dialog window:

The 2nd row of the toolbar contains some radio buttons, used to select the verification engine (in this case, "BMC" or "KLIVE"), and the parameters for the engine (in this case, the "BMC bound"). Below the toolbar, there are two sections: "Property List" (containing the list of properties that can be selected) and "Fault List" (showing the set of faults that can be injected in the model).

To start verification, the user can perform the following steps:

• Select one property from "Property List" by clicking on the corresponding radio button (TIP: Keeping the mouse over a property item in the list, a tooltip will appear, showing the definition of the corresponding property).
• (optional) Check the "Extend Model with Fault Injections" (When checked, it enables the "Fault List" section, which is an expandable tree-view list of the injected faults. By default, the first fault in the list is already expanded).
• Select the desired engine and parameters.
• Click on "Run PV".

As a result of the verification task, the GUI will either show a message in the status bar saying that the property has been found true (possibly up to a given bound) or it will open the trace viewer showing a counterexample trace. In our example, the trace viewer will be opened with the following trace.

Fault Tree Analysis

As another example, we show how to run Fault Tree Analysis. It can be run from the "Safety Fault Tree Analysis" tab.

The user can select the property (corresponding to the top-level event in the fault tree), the verification engine and the corresponding parameters. The result of the analysis is a fault tree, which is opened in the fault tree viewer, along with a probability formula (the formula corresponding to the probability of the top-level event, in python format), which can be displayed by clicking on the corresponding message at the bottom of the GUI window.

The complete list of verification and validation analyses available in COMPASTA are listed in more detail in the following section.

Modeling and Verification Iterations

If the results of formal verification are not satisfactory, it is possible to iterate over the modeling and verification phases. For instance, it is possible to introduce additional redundancy in the system, to prevent single points of failure.

TASTE Workflow

The remaining part of the workflow consists in the standard TASTE workflow, i.e. deployment of the system on the target HW, code generation, testing, etc. For this purpose, the following steps can be executed.

Compilation-Ready Model Transformation

The model must be transformed by removing the HW components, and placing them with corresponding "HW I/O Components". The latter represent the interface components between SW and HW and can be modeled as SW components in TASTE.

Deployment and Code Generation

Using TASTE, it is possible to specify the deployment view and perform code generation.

Testing and Simulation

Finally, the resulting system can be tested and simulated.

Analyses Reference Guide

This section provides a reference guide to the formal analyses that are available in COMPASTA.

Formal analyses are inherited from COMPASS. Full details on the specific analyses can be found in COMPASS User Manual[9]. Examples of use and a tutorial on the use of formal analysis in the design process can be found in the COMPASS Tutorial [10].

Requirements Analysis

Consistency

Checks the consistency of a set of requirements

Inputs:

• A set of requirements

Parameters:

• Engine: MSAT or IC3
• SAT bound (default 10)

Output:

• A witness trace showing that the requirements are consistent, or a message saying that it was not possible to prove that they are consistent

Possibility

Checks that a set of requirements is compatible with another requirement

Inputs:

• A set of requirements
• A requirement (possibility)

Parameters:

• Engine: MSAT or IC3
• SAT bound (default 10)

Output:

• A witness trace showing that the requirements are compatible, or a message saying that it was not possible to prove that they are compatible

Assertion

Checks that a set of requirements implies another requirement

Inputs:

• A set of requirements
• A requirement (assertion)

Parameters:

• Engine: MSAT or IC3
• SAT bound (default 10)

Output:

• A counterexample trace showing that the assertion does not hold, or a message saying that it was not possible to prove that the assertion is implied

Contract-Based Analysis

Validation

Consistency

Checks the consistency a a set of contracts

Inputs:

• A set of contracts

Parameters:

• Engine: BMC or KLIVE
• SAT bound (default 10)
• UnsatCores (if set, generates UNSAT core showing inconsistency)
• Whole Architecture (if set, checks consistency of contracts of the whole architecture)
• Component
• All Contracts of all Components (if set, the check applies to all components)

Output:

• A counterexample trace showing that the contracts are consistent, or a message saying that it was not possible to prove that they are consistent

Possibility

Checks that a set of contracts is compatible with another contract

Inputs:

• A set of contracts
• A contract (possibility)

Parameters:

• Engine: BMC or KLIVE
• SAT bound (default 10)
• UnsatCores (if set, generates UNSAT cores in case a counterexample is generated)
• Whole Architecture (if set, the check is run on the whole architecture)
• Component

Output:

• A counterexample trace showing that the contracts are compatible, or a message saying that it was not possible to prove that they are compatible

Assertion

Checks that a set of contracts implies another contract

Inputs:

• A set of contracts
• A contract (assertion)

Parameters:

• Engine: BMC or KLIVE
• SAT bound (default 10)
• UnsatCores (if set, generates UNSAT cores in case the check succeeds)
• Whole Architecture (if set, the check is run on the whole architecture)
• Component

Output:

• A counterexample trace showing that the assertion does not hold, or a message saying that it was not possible to prove that the assertion is implied

Contract Refinement

Checks the validity of a set of contract refinements

Inputs:

• A set of contract refinements

Parameters:

• Engine: BMC or KLIVE
• SAT bound (default 10)
• Component
• All Refinements of all Components (if set, the checks applies to all components)

Outputs:

• A message saying that the refinements hold, or a counterexample trace if they do not

Tightening

Tightens a set of contracts

Inputs:

• A set of contract refinements

Parameters:

• Top-Down (weakening the assumption of the parent contract and the guarantee of its subcontracts) or Bottom-Up (strengthening the guarantee of the parent contract and the assumption of its subcontracts approach
• Shared Subcontract (consider other contracts refinements which have subcontracts in common)
• Component

Outputs:

• List of tightened contracts

Correctness

Property Verification

Checks if a property holds in the model

Inputs:

• A set of properties

Parameters:

• Engine: BMC or KLIVE
• SAT bound (default 10)
• Extend Model with Fault Injections

Outputs:

• A message saying that the property holds (up to bound), or a counterexample trace if it does not

Contract Verification

Checks if a contract holds against its implementation

Inputs:

• A set of contracts

Parameters:

• Compositional Verification/ Contract Refinement/ Monolithic Verification
• Engine: BMC or KLIVE or KZENO
• SAT bound (default 10)

Outputs:

• A message saying that the contract holds (up to bound), or a counterexample trace if it does not

Safety

Fault Tree Analysis

Generates a fault tree, from a given property

Inputs:

• A property (top level event)

Parameters:

• Engine: SAT or ParamIC3
• SAT bound (default 10)

Outputs:

• A fault tree and a probability formula

Failure Modes and Effect Analysis (FMEA)

Generates an FMEA table, from a list or properties

Inputs:

• A set of properties

Parameters:

• Compact FMEA
• Cardinality
• SAT bound (default 10)

Outputs:

• An FMEA table

Hierarchical Fault Tree Generation

Generates a hierarchical fault tree, from given contracts

Inputs:

• A contract

Parameters:

• Engine: BMC or KLIVE
• SAT bound (default 10)
• Component
• All Contracts of all Components (if set, the check applies to all components)

Outputs:

• A hierarchical fault tree

FDIR

Fault Detection Analysis

Generates a set of alarms (detection means) from a a property

Inputs:

• A property

Parameters:

• SAT bound (default 10)
• Detection delay: Finite or Fixed (value)

Outputs:

• A set of alarms

Fault Isolation Analysis

Generates a set of fault trees from the given list of alarms

Parameters:

• SAT bound (default 10)

Outputs:

• A set of fault trees

Fault Recovery Analysis

Checks if a (recovery) property holds in the model

Inputs:

• A property

Parameters:

• Engine: BMC or KLIVE
• SAT bound (default 10)

Outputs:

• A message saying that the property holds (up to bound), or a counterexample trace if it does not

Diagnosability Analysis

Checks if a property is diagnosable in the model

Inputs:

• A property

Parameters:

• Engine: MSAT-BMC or IC3
• SAT bound (default 10)

Outputs:

• A message saying that the property is diagnosable (up to bound), or a counterexample (pair of traces) if it does not

Demo Video

A demo of COMPASTA can be watched here [11]