Detail

dc?++ Model Checker

One fundamental idea of service-oriented computing is that applications should be developed by composing already available services. Due to the long running nature of service interactions, a main challenge in service composition is ensuring correctness of failure recovery.
dc?++ is a process calculus suitable for modelling long running transactions, within the framework of ?-calculus, with a recovery mechanism based on compensations. This is supported with a tool for verifying the correctness of failure recovery, under a notion of compensation correctness.
The software is a Prolog interpreter for dc?++ specifications, which includes a parser and the encoding of the labelled transition system that, used together with ProB model checker, allows to verify the correctness of long running transactions. Therefore, the developed software includes a Prolog interpreter for dc?++ calculus and the encoding of the labeled transition system rules.