In Chap. 10, it has been shown how
can deal with the static verification of ConDec models. In order to assess the usability of the proposed approach, it is necessary to evaluate its performance and scalability, comparing it with other verification techniques. This chapter aims at showing that
technology when it comes to the static verification of ConDec models. An extensive experimental evaluation is presented, stressing
and emphasizing its performance results in both favorable and unfavorable cases. After having discussed how the static verification task can be also interpreted as a model checking problem, we compare
with state-of-the-art explicit and symbolic model checkers, providing an empirical discussion of their benefits and drawbacks.
The presented benchmarks will stress the scalability and performance of the verification techniques along two significant dimensions:
size of the model
(number of mandatory constraints contained in the model);
cardinality on activities
(presence of existence constraints requiring a minimum number of executions of some activity in the model).
All experiments have been performed on a MacBook Intel CoreDuo 2 GHz machine, and considering the SICStus-based implementation of