Verification

CLIMB exploits different Logic-Programming based techniques in order to verify and reason upon CLIMB models. In particular, CLIMB adopts:

SCIFF to perform static and (run-time/a posteriori) conformance verifications, to reason upon interoperability and even to enact CLIMB models (ongoing work);
Prolog to perform a posteriori conformance verification and classify execution traces;
Inductive Logic Programming techniques to mine CLIMB models starting from execution traces, previously labeled as compliant or not.

DecSerFlow

DecSerFlow/Condec models already have an underlying semantics in terms of Linear Temporal Logic, making possible to exploit model-checking techniques for verification. Conformance checking, static verification, interoperability and enactment of basic models are therefore addressed with LTL as well. For more informations, visit the DECLARE and ProM web-sites!

CLIMB

Computational Logic for the verIfication and Modeling of Business processes and choreographies

Sections

Verification

DecSerFlow