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

using constraints. The constraints set variables in relations using some operators,
and in this way they form expressions. Various types of expressions can be used
to define constraints (e.g. Boolean, SMT - depending on supported features of the
solver). The solution of the CSP sys is a set of values of X CSP for which all constraints
C CSP are satisfied. The constraint solver performs the task of finding solutions.
In order to represent the composition M sys in a CSP, we need to map the top-
level contract structure ((sub-)contracts, variables, and A/G expressions) into the
CSP constructs mentioned above. Important aspects of this representation are CSP
definitions for (1) a type system, (2) A/G expressions or properties, (3) the structure
of components and contracts and (4) the structure of compositions. We can now turn
to these representations.

3.4.1 Type System

The CSP tools, i.e. constraint solvers, usually provide the support for several do-
mains to represent various types of variables. Integers, reals, and sets are examples
here, just to name few. In order to avoid type castings between modelled system M sys
and CSP sys , we use the same domains for both M sys and CSP sys . Another reason is
that the time needed for the constraint solver to solve the CSP strongly depends on
a particular domain. For example, there is a significant difference in runtime when
dealing with real numbers instead of integers. Therefore, we use integers for both
system representations, i.e. M sys and CSP sys .

3.4.2 A/G Expressions (Properties)

Concerning the representation of values of variables in the CSP, limits have to be
set on their intervals. The intervals are possible search space for the solver, and can
have significant influence on solver's runtime. It is therefore important to limit the
variables on smallest possible intervals.
In our CSP sys , each variable which is used in an expression is represented by two
CSP variables: one indicating the begin of the interval, another one for the end of
that interval. The size of this interval is determined based on intervals defined in ex-
pressions. For example, the variable s en in the expression

( 0 ≥ s en ≤ 6400 ) is limited

on the interval . The reason for using two CSP variables here is that solving

the CSP results with not only decision about the correctness of a composition with
regard to the relation (5), but it also provides values for which the relation (5) is
satisfied. In this way, we can obtain the concrete intervals (instead of just values)
for all variables in all contracts (for correct compositions). This information can be
useful for example when the composition M sys has many alternative contracts, to
observe which of them are identified as correct.
Relations or operations between variables in expressions are represented as
constraints. Since both M sys and CSP sys use the SMT syntax for expressions, every
operation is represented as a single constraint.

[ 0 , 6400 ]