First-Order Dynamic Logic for Compensable Processes
Jun 2012
Compensable programs offer a convenient paradigm to deal with long-running
transactions, because they offer a structured and modular approach to the
composition of distributed transactional activities, like services. The basic idea is
that each activity has its own compensation and that the compensable program
fixes the order of execution of such activities. The main problem is how to guarantee
that if one or even many faults occur then the compensations are properly
executed so to reach a consistent configuration of the system. We propose a formal
model for such problems based on a concurrent extension of dynamic logic
that allows us to distill the hypothesis under which the correctness of compensable
programs can be ensured. The main result establishes that if basic activities
have a correct compensation we can show the correctness of any compound compensable
program. Moreover, we can use dynamic logic to reason about behavioural
and transactional properties of programs.
