Constraint-Based Verification of Compositions in Safety-Critical Component-Based Systems - Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing - page 113

be described. For example, the property in Figure 1 may include some additional
parameters to define conditions for the t ig more precisely.

•

Alternatives : properties may have alternative representations for different context
(e.g. the Injection System component M IS can provide different properties for
different engine types).

These relations have to be supported when modelling a component-based system
and they have to be considered when such a system has to be verified.

3 Constraint-Based Verification

In this section, we describe the proposed approach for compositional verification.
To get a rough image of our approach, we summarized the basic steps in Figure 2

Component-based System Msys Constraint Satisfaction Problem

CSPsys
Constraint

M - Component

M

1 - Transform

Variable

M M

M
M M

Variable

Constraint

CONSTRAINT
SOLVER

Satisfied

Not satisfied

2 - Verify

Fig. 2 Overview of the proposed verification method: (1) transformation of the component-
based system M sys into the CSP representation CSP sys , (2) verification of the composition
CSP sys by solving a CSP

that we perform to conducts the verification process. The input to the verification
is a modelled component-based system, enriched with properties - M sys in figure.
This model is further transformed into a Constraint Satisfaction Problem (CSP) -
CSP sys in figure, which is a network of inter-connected variables and constraints
(we discuss this later). The CSP model is processed by the constraint solver, i.e. a
tool to solve the CSPs, in order determine the preservation of all properties in the
system. As a result, we get a decision about such a preservation. In addition, we get
concrete values of data (i.e. inputs, outputs, parameters), for which properties are
preserved. All steps in the process are performed automatically.
In the following, we describe how we defined each model described above. We
first give some basic assumptions for our system M sys . Then we describe the main
elements of that system, including properties. In the end, we describe its represen-
tation as a CSP.