Conformance Checking aims at verifying whether a concrete process execution (or service interaction) complies with the prescribed model.
In a business process setting, it checks if performed activities meets a set of ConDec constraints. In a SOA setting, it can be exploited both to verify the behaviour of a single service or, by collecting the whole exchanged messages, to check if a service composition follows the choreography’s rules of engagement.

The SCIFF proof-procedure is able to perform conformance checking both:

• at run-time, by dynamically collecting occurring events. In this way, violations are detected as soon as possible, and SCIFF can be adopted as an alerting infrastructure;
• a-posteriori, by analyzing already finished executions, i.e. a set of execution traces. In this respect, rules are used as an intuitive classification criterion which split analyzed traces in compliant and non compliant.

To improve performances, a-posteriori verification of CLIMB models has been realized in pure Prolog as well (this is possible because analysis of already completed execution traces does not require SCIFF’s reactivity anymore).