CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  Prototypes  \  Prototype Page Login  
banner bottom
File Top
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.

Authors: Carla Ferreira
File Bottom