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

contracts, i.e. ( C FS ⊗ C IS ) ⊗ C IIAS ) C II . Note that only the relation with the

contract C IS is highlighted here.

•

Alternatives : when designing components for more than one context, each new
context is described in a separated contract. Contracts that describe the same
property for different context are alternatives. In example in Figure 3, any of
contained contracts may have alternatives - here, we just highlighted C FS to in-
dicate that it may have alternative contracts.

Based on definitions for contracts and their relations, we can now define the top-
level system/composition contract, C sys , as follows:

C sys : =( ⊗ i ∈ N C i ) (3)

, i.e. a hierarchical composition of contracts C i ,where C i represents further compo-
sition according to relation (3).
Finally, to relate contracts with components, i.e. the concrete implementations of
contracts, we extend the relation (1) as follows:

= Σ M c

in out par

M : , Σ , Σ , C c , (4)

,where C c is a set of contracts that the component M can implement. Based on this
relation, any implementation of the C sys contract represents a complete component-
based system or a top-level composition. We identify this implementation as M sys
and use it later as a basis to define our CSP.

3.3 Ensuring Correctness of Compositions

For our component-based system defined previously, two contracts C 1 and C 2 can
form a composition (i.e. can be integrated) when their connected assumptions/guar-
antees match in the syntax of their variables (i.e. datatypes, units, etc.), and when
following holds:

G ( C 1 ) ⊆ A ( C 2 ) (5)

In other words, the contract C 1 shall not provide values not assumed by the contract
C 2 . This relation is a basis in our CSP to verify the complete composition.

3.4 Composition as a Constraint Satisfaction Problem

Now, we describe how we define the composition M sys as a CSP. We name our CSP
representation of M sys as CSP sys , and define it as follows:

CSP sys : = X CSP , D CSP , C CSP (6)

,where X CSP is a finite set of variables, D CSP their domains (datatypes, values),
and C CSP a set of constraints related to variables and constraints in C CSP .Inother
words, the CSP represents a network of variables inter-connected with each other