Example

The approach of the Eclipse CommaSuite project is illustrated by an example of an imaging system. The example is available in the tooling, see the section on Examples in the user guide. More details of all aspects can be found in the user guide.

The imaging component has three provided interfaces and 2 required interfaces as shown in the next figure.

image

First we discuss the specification of the IImage interface and what can be done based on this specification. Next we discuss the specification and analysis of the Supervision component.

IImage interface

For the IImage interface, we present the specification, the analysis of the model using checks and simulation, document generation, and monitoring.

Specification

Interface specifications may use non-primitive types which can be declared in files with extension .types. As an exmple, we use file Basic.types with following contents:

/*
 * Return type of commands
 */
enum Result {
    Ok        // Successful execution of command
    Error     // An error occurred when executing command
}

Next we define the signature of the interface in a file with extension .signature, i.e., the commands and signals that can be called by clients of the interface, and the notification that can be sent to the client. Note that comment have been added including certain keywords; this can be used by document generation. This leads to the following file IImage.signature.

import "../Basic.types"

signature IImage

commands
/*
 * Prepare image capture
 * \param setting An integer representing detector setting
 * \return Result indicating whether setting is successful or failed
 */
Result Prepare(int setting)

/*
 * Start imaging
 * \return Ok or error
 */
Result StartImaging

/*
 * Unprepare image capture; new image requires new prepare
 */
void Unprepare

signals
/*
 * Asynchronous message to stop imaging
 */
StopImaging

notifications
/*
 * Error notification
 */
Error

The allowed order of the commands, signals and notifications is specified in a file with extension .interface. In addition, also constraints in timing and data can be expressed.

File IImage.interface below shows that the allowed order of the events is specified by means of a state machine. Note that this state machine does not represent an implementation, it is just a way to express the allowed sequences of events. In every state, it is specified which transitions may happen. For instance, in the Initial state only a call of command Prepare__ is allowed. Anything that is not specified should not happen. Triggers are calls of the client to commands and signals. Everything inside the "do" part is performed by the server, such a reply to a command or a notification.

Observe that there are two possible responses to the Prepare call; it is either Ok or Error. This reflects the fact that the specification abstract from the implementation and just defines the possible responses.

For transitions that occur in all states, there is a convenient abbreviation.

At the end of the specification, timing constraints are specified, where the first string is the name of the constraint. For instance, constraint PrepareReply expresses that the reply to a Prepare command should occur between 1 and 8 ms.

import "IImage.signature"

interface IImage version "1.0"

machine ImagingMachine {

    in all states {

        transition
            do: Error
            next state: Initial
    }

    initial state Initial {

        transition trigger: Prepare(int setting)
                do:
                reply(Result::Ok)
                next state: Prepared
            OR
                do:
                reply(Result::Error)
                next state: Initial
    }

    state Prepared {

        transition trigger: StartImaging
                do:
                reply(Result::Ok)
                next state: Imaging
            OR
                do:
                reply(Result::Error)
                next state: Initial

        transition trigger: Unprepare
            do:
            reply
            next state: Initial
    }

    state Imaging {
        transition trigger: StopImaging
            next state: Prepared
    }
}

timing constraints
PrepareReply command Prepare - [ 1.0 ms .. 8.0 ms ] -> reply to command Prepare
StartImagingReplyOK command StartImaging and reply(Result::Ok) to command StartImaging -> [.. 100.0 ms] between events
StartImagingReplyError command StartImaging and reply(Result::Error) to command StartImaging -> [.. 10.0 ms] between events

Model quality checks

The model quality checks can be used to detect modeling mistakes such as unreachable states and race conditions. It requires a .params file with a specification of values for commands and signals with parameters. In this case only a value for the Prepare call in state Initial is needed. We choose to explore the model with input values 13 and 42, which is specified as follows in file IImage.params.

import "IImage.interface"

interface: IImage

trigger: Prepare
state: Initial params: ( 13 ) params: ( 42 )

In general, all generating tasks are specified in a project file with extension .prj. To perform model quality checks we use the following file IImage.prj. Here max-depth limits the exploration to a certain depth.

import "IImage/IImage.interface"

Project IImageProject {

    Generate ModelQualityChecks {
        ModelQualityChecks_IImage for interface IImage {
            params: 'IImage/IImage.params'
            max-depth: 50
        }
    }

}

Running the generator leads to a dashboard with results.

image

It shows that there are a number of race conditions. The next figure shows one of the server races, where an Error notification occurs in parallel with a StartImaging call; this leads to a StartImaging call in the Initial state which is not allowed. This can, for instance, be solved by adapting the state machine to allow this call.

image

Simulation

To validate the specification, a simulation can be generated by the following task in the .prj file:

enerate Simulator {
        Simulator_IImage for interface IImage
        {
            params: "IImage/IImage.params"
        }
    }

Note that it also uses the .params file.

Executing this generator leads to panel which allows the simulation of the interface based on the specified interface, see the next figure.

image

Document generation

Based on the models, including comments, a Word document can be generated. First a template document Template.docx has to be downloaded and the following task in the .prj file can be used:

Generate Documentations {
        documentation for interface IImage {
            template = "Template.docx"
            targetFile = "Documentation.docx"
            author = "John Smith"
            role = "R&D: SW Designer"
        }
    }

This task generates a Word document with, for instance, the signature (including comments)

image

and the state machine, in the form of a table and a plantUML picture.

image

There is also a separate task to generate UML figures only.

Monitoring

By means of monitoring, it is possible to check if an implementation conforms to the specified interface. First client-server interactions have to be recorded in a so-called events file, for instance, by logging or sniffing. The next figure shows a part of trace of the Supervision component in the .events format. An alternative is to use a JSON format.

image

A set of traces in folder EventFilesSupervision, can be monitored by the following task:

Generate Monitors {
        monitoring for interface IImage {
            trace directories "EventFilesSupervision"
        }
    }

This leads to a dashboard which shows whether a trace conforms to the interface specification (green), conforms to the state machine but violates at least one constraint (yellow), or violates the state machine (red).

image

For a violation, more information is provided, see the next figure for a violation of the state machine:

/[#img_violation] image

Note that the dashboard also contains information about the coverage of the state machine. Moreover, for the constraints there are histograms and statistical information, see for instance the next figure:

/[#img_histogram] image

Monitoring is also available as command line tooling such that it can be integrated into the test process.

Component model

A component be specified by means of its proved and required interfaces. In addition, functional constraints on the relation between interfaces can be specified. For instance, for component Supervision we specify that the result of the StartImaging call depends on the states of the Vacuum and Temperature ports.

import "ITemperature/ITemperature.interface"
import "IVacuum/IVacuum.interface"
import "IImage/IImage.interface"
import "IPump/IPump.interface"
import "IAcq/IAcq.interface"

component Supervision

provided port ITemperature iTempPort
provided port IVacuum iVacPort
provided port IImage iImagPort
required port IPump iPumpPort
required port IAcq iAcqPort

functional constraints

StartImagingConstraint {

/*
 * Imaging can start only if vacuum is present and temperature level is reached
 */
 use events
    command iImagPort::StartImaging
    iImagPort::reply to command StartImaging

    initial state Status {
        transition trigger: iImagPort::StartImaging guard: iVacPort in Vacuum and iTempPort in TemperatureSet do:
            iImagPort::reply(Result::Ok) to command StartImaging
        next state: Status

        transition trigger: iImagPort::StartImaging guard: not iVacPort in Vacuum or not iTempPort in TemperatureSet do:
            iImagPort::reply(Result::Error) to command StartImaging
        next state: Status
    }
}

Moreover, time and data constraints can be specified:

timing constraints

StartPumpDelay
command iVacPort::VacuumOn -[.. 20.0 ms]-> command iPumpPort::On

ErrorPropagation
notification iAcqPort::Error - [ .. 3.0 ms ] -> notification iImagPort::Error

data constraints
variables
int val1
int val2
Result r1
Result r2

/*
 * The setting passed to IImage Prepare is used in the
 * IAcq PrepareAcquisition
 */
PrepareValue
command iImagPort::Prepare(val1);
no [command iAcqPort::PrepareAcquisition]
until
command iAcqPort::PrepareAcquisition(val2)
where val1==val2
observe
received := val1
forwarded := val2

PrepareReply
iAcqPort::reply(r1) to command PrepareAcquisition;
no[iImagPort::reply to command Prepare]
until
iImagPort::reply(r2) to command Prepare
where r1 == r2

Component Supervision can be monitored by the following task in the_ .prj_ file:

    Generate Monitors {
        monitoringSupervisionComponent for component Supervision
        { trace directories "EventFilesSupervision"
        }
    }

This monitors all interfaces of the component and all component constraints, leading to a dashboard:

image