This chapter is devoted to discuss how the
proof procedure can be adopted for the static verification of ConDec models. The scalability of the approach will be investigated in the next chapter.
The first part of the chapter demonstrates how existential and universal properties, as defined in Sect. 8.3.1, can be expressed in CLIMB and verified with
. Thanks to this possibility,
can be exploited to deal with all the static verification tasks introduced in Chap. 8:
discovery of dead activities;
checking the executability of composite models;
verification of conformance to a choreography.
The second part of the chapter is instead focused on termination issues; as sketched in Sect. 9.4.3, the termination of
cannot be generally guaranteed when reasoning upon CLIMB specifications, and therefore an ad-hoc solution for ConDec must be provided.