Automated Checks

Overview

At the DLR Laboratory a framework to run regular checks is running on a regular schedule with the goal to perform all SCADE based proof and tests on a regular agile schedule.

The current scedule is: 60 minutes triggered by changes in the modeling repository

Cloning the modeling and the validation repository should reside inside the same directory so that the includes can be reconstructed in other working environments.

Nightly Verification Setup

To enter the tests or the proof a configuration needs to be filled out and placed in the folder of you root verification node. A template to this file can be found at: https://github.com/openETCS/validation/tree/master/Templates/NightlyVerificationSetup.csv .

A short description of the rows can be found below:

*.etp project file with full path

This column is giving the *.etp file to code generate and complie for test reasons. It can be the path and the filename to the verification object (DAS2V) or to the verification model.

Verification Object::root node (mandatory)

This column contains the SCADE root node of the object to verification. It should reside at the modeling repository. Should be described by the *.etp file with the SCADE node (usually an operator or root node).

Initial Github Hashtag of DAS2V (mandatory)

This column contains the full length git hashtag of the modeling repository. The Hashtag describes the first valid commit the verification is applied on. From this time on the verificaiton should hold. It is used to roll back and sustainably answer the question: From which time on did the error occur.

Verification Model::root node (mandatory)

This column contains the SCADE root node of the verification definition. It should reside in the verification repository. It can be used to define the interface contract in case of static sss scripts.

Conventions for the Verification Model::root node

To be able to automatically process the results from a verification model, some conventions were agreed on.

1. All verification activities are divided into user stories.
2. Every verification result shall have a dedicated output on root level.
3. Every output describing a verification result shall start with "US_" (User Story) following a name of the verification complying to the verification specification.
4. The result of the complete output should be called "US_OK" and have the typer boolean.
5. The result shall be interpreted on a false = failed and true = passed convention.
6. The value of US_OK shall be persitant false. Once the result is false it shall stay false for the rest of the run.
7. The root node shall have a boolean output called ready. ready = true shall indicate the end cycle of the verification related to the verification model

Verification Model Input (optional)

Relative repository path + filename insice validation reporitory to the sss script in case static input is required. Static input covers the changes of variables inside the scade model during execution of validation.

Even if only sss scripts are delivered as verification definition In case SSS scripts are utilized, All types of this object should reside in the validation repository.

Observable File (optional)

Contains the variables for logging reasons. Can be automatically generated from the SCADE watchlist during Simulation. Should containt all proof outpus. This file is only needed if obervables beyond the inputs and outputs to the Verification Model::root node are needed.

Verification Goal (mandatory)

Please describe the goal of the verification. the level of quality can be:

• Functional Correctness
• Operational Correctness
• Correctness of Engineering Rules
• Safe Behaviour of the System

Verification Level (mandatory)

State the level of verification. e.g. Module Verification according to EN 50128