Difference between revisions of "COMPASTA: Integration of the TASTE and COMPASS toolsets"

From TASTE
Jump to: navigation, search
(Introduction)
(COMPASTA Workflow)
Line 33: Line 33:
  
 
:[[File:ClipCapIt-221111-103947.PNG]]
 
:[[File:ClipCapIt-221111-103947.PNG]]
 +
 +
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.
 
The COMPASTA workflow is composed of the following steps.
Line 45: Line 51:
  
 
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".
 
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. First, we set the Slim language to a function block by right-clicking on the block and by selecting "Properties" from the contextual menu.
 +
 +
:[[File:ClipCapIt-221111-111123.PNG]]
 +
 +
The "Properties" window appears. Slim can be set as implementation language in the tab "Implementations".
 +
 +
:[[File:ClipCapIt-221111-111419.PNG]]
 +
 +
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.
 +
 +
:[[File:ClipCapIt-221111-111724.PNG]]
 +
 +
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.
 +
 +
:[[File:ClipCapIt-221111-111850.PNG]]

Revision as of 10:19, 11 November 2022

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.

ClipCapIt-221111-102354.PNG


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.

Installation

COMPASTA can be installed on a Debian 10 or Debian 11 Virtual Machine. Installation within the VM requires the user to clone the taste-setup repository (branch compasta_feature_bullseye) and install TASTE as follows:

    $ git clone https://gitrepos.estec.esa.int/taste/taste-setup.git tool-src
    $ cd tool-src 
    $ git checkout compasta_feature_bullseye 
    $ ./Update-TASTE.sh

Further installation instructions will be added when COMPASTA is publicly released.

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.

ClipCapIt-221111-103947.PNG

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.

ClipCapIt-221111-103701.PNG

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. First, we set the Slim language to a function block by right-clicking on the block and by selecting "Properties" from the contextual menu.

ClipCapIt-221111-111123.PNG

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

ClipCapIt-221111-111419.PNG

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.

ClipCapIt-221111-111724.PNG

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.

ClipCapIt-221111-111850.PNG