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

of the refined/abstracted or alternative contracts (contract parts Cs p in figure). Be-
cause refined/abstracted and alternative contracts do not depend on each other, we
define the top-level constraint C s as follows: C s :

=( ∨ i ∈ N Cs pi )

. In this relation, any
contract which can satisfy the relation (5) implies that the top-level contract con-
straint C s is satisfied.
As illustrated in Figure 4, every contract consists of the following sub-constraints:

• A/G constraints C agc : constraints related only to local A/G variables. These con-

straints define the assumptions and guarantees for a contract. They are defined
based on A/G expressions in contracts, as described in Section 3.4.2.

• Binding constraints C bc : constraints that link the local A/G variables to the global

component variables so that both types of variables get the same values. In this
way, we can observe which contracts were satisfied, after successful verification.

• Composition constraints C cc : constraints that integrate the contracts. These con-

straints express the integration or composition between two contracts, as de-
scribed in Section 3.3. They link two contracts according to relation (5).

All three top-level constraints have to be satisfied for a contract C sp ,i.e. C sp : =

( .

Finally, the top-level constraint of a component is satisfied, if all contract con-
straints C s are satisfied, i.e. C m :

C agc ∧ C bc ∧ C cc )

=( ∧ i ∈ N C si ) .

3.4.5 System/Composition

The compositions have very similar structure to basic or atomic components. Be-
cause they abstract some contracts of the contained components, additional con-
straints are defined to link these variables. An example of such a composition is
given in Figure 3, where assumptions and guarantees of the contract C II are an ab-
straction of assumptions and guarantees of the contained contracts.
Like atomic components, the complete component-based system M sys is repre-
sented in a CSP as a set of variables and constraints. Within this set of constraints,
there is a single top-level constraint of the composition C m which links the complete
hierarchy of the sub-constraints and variables discussed previously. The CSP has a
solution only if this top-level constraint is satisfied. Finally, the C m corresponds to
the top-level constraint in the constraint set C CSP from the relation (6).

4 Experimental Results

In the following, we describe the results of the preliminary evaluation and we dis-
cuss the performance of our approach.
To conduct the experiment, we used Java-based Choco constraint solver
(choco Team (2010)). In our experiment, we defined the composition M sys as a XML
description, which is then used to generate the CSP in memory.
The main goal of this experiment is to show whether the proposed CSP is appli-
cable to solve the composition problems defined with data properties, and for which