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

and these expressions are alternatives (as mentioned in the description of the mea-
surement). The response time of the verification strongly depends on the number of
alternatives, because each of the expressions represents different interval. The solver
has to adjust the component variables to adequate intervals, in order to find a solu-
tion. Furthermore, since the choice of the particular alternative may influence the
choice of the intervals in other connected components, often the backtracks have to
be done to the state where the constraints were satisfied, which is time consuming.
In the second measurement, we observed very similar results as illustrated in
Figure 6 on the left. Having fixed values on component variables, no search has to
be performed, but just the constraint verification. For the case where the alternatives
are used, more time is required to find a solution, but this time is negligible in
contrast to situation when using intervals (i.e. Figure 6, right).
In the end, we summarize our observations with Figure 7. This figure shows the
region for which the verification can complete in a ”reasonable time”. We set the
limit for this time on 2 minutes, just to get a first feedback about possible con-
figurations for the system under test. To establish this region, we used the system
configuration with the worst case in response time, i.e. the one having the alternative
properties from the first measurement.

4.2 Qualitative Results: Discussion

Figure 7 shows the worst-case scenario, in which a component-based system is
modelled having varying number of assume guarantee expressions. The verification

350

300

250

200

Not usable configurations

150

100

Response time < 2 min

50

0

0 50 100 150 200 250 300

# of components

Fig. 7 Region of possible system configurations for which the verification completes within
a given time

scales well but for configurations with only few instances of either components or
properties. In nowadays automotive systems for example, there are more than 800
software components, that control various technical sub-processes in automobiles