Compensable Programs - Formal Methods and Hybrid Real-Time Systems - page 350

The π -calculus has been applied in describing various compensable program
models. Lucchi and Mazzara formalised the semantics of BPEL within the frame-
work of the π -calculus [18]. Laneve and Zavattaro explored the application of the
π -calculus in the formalisation of the compensable programs and the standard
pattern of compisition [16].
This paper is an attempt at taking a step forward to gain some perspectives
on compensable programs within the design calculus [14] as well as to identify
the links among various models for the following language features

- Exception handling
- Compensation mechanism

Our contributions include

- providing a conservative extension of the standard relational model to deal
with fault handling and compensation, which can be characterised by addi-
tional halthiness conditions.
- exploring the algebraic system for exception handling and compensation.
- constructing a Galois connection (retract) to link the new model with the
design model.

The paper is organised as follows: Section 2 defines the merge combinator of de-
signs, which is used later to construct design matrix in describing the dynamic
behaviour of compensable programs. It also investigates the algebraic proper-
ties of the merge operator. Section 3 presents the new healthiness conditions to
capture the exception handling and compensation features of compensable pro-
grams, and introduces a new notion design matrix . It also explores the Galois
link between the design model with the design matrix model. Section 4 gives an
observation-oriented semantics to compensable programs. We explore the alge-
braic properties of exception handler and compensation mechanism in Section 5.
The paper concludes with a short discussion on the linking theories.

2 Preliminaries

This section introduces some notations which will be used in constructing design
matrix in the next section.
Definition 2.1 (Merge)
Let P and Q be designs. The notation P

⊕ Q denotes the program which merges

the outcomes of P and Q .

P ⊕ Q = df if ( pre .P → P, pre .Q → Q ) fi

where pre .P stands for the precondition of Design P :

P [ true, f alse/ok, ok ]

pre .P = df

¬

Theorem 2.1. ( b S ) ⊕ ( c T )= df ( b ∨ c ) ( b ∧ S ∨ c ∧ T )