|Home \ Prototypes \ Prototype Page||Login|
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.
Date: January, 2011
Authors: Carla Ferreira