Formal specification, verification and analysis of long-running transactions

Compensation-based long-running transactions (LRTs) are the main error recovery mechanism in business process modelling languages. Correctly implementing LRTs is difficult, especially in a concurrent setting. To ease this task we are developing a full-fledged formal approach to the description, design, analysis and verification of long-running transactions. The existing calculi Sagas and compensating CSP rely on different compensation policies regarding concurrent processes. Unfortunately they either require synchronization before compensating or they include unrealistic traces. We therefore propose a new policy that improves existing ones using realistic distributed compensations. In this thesis we formalize the behaviour of the new policy using three semantics: i) a denotational semantics to compare it with previous policies, ii) an operational semantic based on an encoding into Petri nets as a foundation for richer semantic domains that record causal dependencies between events, iii) an easily extendable small-step SOS semantics, that facilitates model checking. We prove the correspondence between the different semantics showing their observational equivalence. Moreover we develop a tool for each of the semantics in Maude to improve and validate our theory. Finally, we introduce a logical framework to model and analyse LRTs based on dynamic logic. We use it to derive sufficient conditions under which a compensable program is guaranteed to restore a correct state after a fault