dcπ++ : a dynamic compensation calculus

  • dc&pi++ is a calculus for modeling long running transactions within the framework of &pi-calculus, with support for compensation as a recovery mechanism.

Syntax

operators dc&pi syntax ASCII syntax
Inaction
{\bf 0}
 inaction
Output
\overline{a}\langle v_1,...v_n\rangle
a<v1,...,vn>
Failure
\overline{t}
t< >
Variable
X
 hole
Input guarded choice
a_1(x_1,...,x_n_1)\left\lfloor\lambda X . Q_1 \right\rfloor . P_1 +
a_2(y_1,...,y_n_2)\left\lfloor\lambda X . Q_2 \right\rfloor . P_2
(a1(x1,...,xn1)%Q1).P1 +
(a2(y1,...,yn2)%Q2).P2 (*)
Parallel composition (**)
P \, | \, Q
P | Q
Restriction
( \sigma x) P
(x)(P)
Transaction scope
t[P,Q]_{r}
t[P,Q]r
Protected block
\langle P \rangle_{r}
<P>r
(*) The parentheses can be ommited if the process Q1 is simple, such as inaction, output, failure,
hole or input without prefixing.
(**) The operator | has more precedence than the prefix operator. For the contrary we use parentheses,
i.e., a(x).P | Q &ne a(x).( P | Q ).

How to use dc&pi++ for model checking

The software icomp.sh is a Prolog interpreter for dc&pi++ 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.


You should use ProB distribution for linux, which includes probcli command.


Keep on the same directory icomp.sh and probcli executables.


You need to update the variable PROBCMD at the beginning of the script.


Usage: ./icomp.sh example.pi example.map prop.ltl


The file example.pi is a dc&pi++ specification written in ASCII. The correctness map is described in example.map. The file prop.ltl specifies the linear temporal logic (LTL) formula that express the correctness property for example.pi. The LTL formula is written according to ProB syntax, namelly is written is LTLe, an extended version of LTL supported by ProB.

dc&pi++ examples


Contacts

If you have any questions, please email:
cvaz_at_cc.isel.ipl.pt