Static verification is an a-priori reasoning process which aims to check model’s consistency.
Following the work of Pesic et al., mainly two kinds of consistency verification are addressed in CLIMB:

• conflicts detection, which aims to check consistency of the whole model, i.e. to ensure that at least one execution is accepted
• discovery of dead activities, which aims to find local inconsistencies inside a model, namely to discover the set of activities that cannot be executed at all.

Such verifications are extremely important in case of composite models (see interoperability).

In order to detect conflicts, a generative version of SCIFF, called g-SCIFF, is exploited. Starting from a given goal (in terms of expectations) it is capable to simulate an execution trace which satisfies model's constraints. In this case, g-SCIFF is simply applied on the CLIMB model with the goal true. Generation is then driven by the presence of constraints which impose to perform a given activity independently from execution (such as the existenceN constraint). Execution of these activities are simulated, new constraints could be triggered, and so on. If a compliant execution trace can be finally generated, then the model does not contain conflicts.

Discovering whether a certain activity is dead is a very similar task: it can be reduced to conflicts detection by imposing as goal that the activity will be executed at least once. This exactly corresponds to detect conflicts on the CLIMB model obtained by adding to the original one an existence1 constraint on the activity under test.

The figure below shows an example of dead activities inside a DecSerFlow model.