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

of components, each having varying number of properties but with constant number
of assumptions or guarantees (i.e., each component variable is therefore related to
only one expression). In the second part, each of the components has varying num-
ber of alternative and refined properties, so that many solutions are possible. In this
case, each component variable is related to many expressions.
The expressions in the first measurement are defined in a way that always the
intervals of the component variables have to be satisfied, and not the fixed values.
An example for such expression is given in Section 3.2 for the contract C II ,whichis
satisfied only if the variables s en and a tr are in ranges [ 0 , 6400 ] and [ 0 , 100 ] respec-

tively.
For the input test data, i.e. the operands of the assumption and guarantee expres-
sions, we generate the values for each expression randomly, but with the rule that
the assumptions are always satisfied. The advantage of performing the positive tests
here is to get more clear statement about the runtime of the verification. In both parts
of the measurement, we use the relational and logical operations on values.
In the second measurement, we execute the same system configurations as in
previous measurement, but this time using the fixed values for component variables.

4.1.2 Observations

First results of the experiments are illustrated in Figure 6. On the left, an excerpt of
the results for the first measurement is shown, where the properties have a constant
number of assumptions and guarantees. The reason why the verification responds in

70000

1600

1400

60000 # alternat ives per component

4
6
8

# compon ents
10
20
50

1200

50000

1000

40000

800

30000

600

20000

400

10000

200

0

0

400 800 1200 1600 2000
# of assumptions/guarantees per component

0 200 20 400 40 600 60 800 80 1000 100

0 20 40 60 80 100 120

# of components

Fig. 6 Experimental results: runtime for system configuration with varying number of as-
sumption/guarantee expressions and components (left) and varying number of components
and alternative properties (right)

short time is that each component variable has only one expression (assumption or
guarantee constraint, C agc ), and it is then immediately instantiated to a value indi-
cated by that expression. The runtime depends in this case therefore on the number
of components and properties.
On the right in Figure 6, a scenario that is more likely to occur in practice is
shown. Here, each component variable has an increasing number of expressions,