Logo eprints

Formal specification, verification and analysis of long-running transactions

Kauer, Anne Kersten (2013) Formal specification, verification and analysis of long-running transactions. Advisor: Bruni, Dr. Roberto. Coadvisor: Ferreira, Dr. Carla . pp. 215. [IMT PhD Thesis]

Kauer_phdthesis.pdf - Published Version
Available under License Creative Commons Attribution No Derivatives.

Download (1MB) | Preview


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

Item Type: IMT PhD Thesis
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
PhD Course: Computer Science and Engineering
Identification Number: 10.6092/imtlucca/e-theses/117
NBN Number: urn:nbn:it:imtlucca-27150
Date Deposited: 27 Jan 2014 11:17
URI: http://e-theses.imtlucca.it/id/eprint/117

Actions (login required, only for staff repository)

View Item View Item