Compiling compensating automata

Abstract

A compensation is a means of undoing the effect of some previously completed action, similar in its use to roll-backs. Compensations however, need not be the exact opposite of the action they remove the effect of like it is the case for roll-backs. Compensations are also useful in more scenarios when compared to roll-backs such as when external entities are involved or when needing support for undoing or cancelling in long-running transactions. There are many ways that can be used for describing compensations such as the using of StAC and CHTTA formalisms. However, only the use of compensating automata allows for the strict separation of the system logic from the compensation logic. This separation allows for the system and its compensations to lie in different modules, hence permitting the addition of compensations to a system that does not have them with the use of monitor oriented programming. Before this project was started, there was no implementation of compensating automata that we could make use of. This is the reason why we wanted to carry out this project in the first place. With this work, we aim to find an encoding with which to compile compensating automata into something that can be run, and so to be able to use compensating automata to provide compensation support for a running system. We also aim to design a syntax that may be used for describing collections of compensating automata in a formal textual way as well as to use the compilation process developed to implement a case study. With the case study, we aim to gain more confidence in compensating automata by making use of them in a practical real-life scenario. While carrying out this work we have managed to implement a compilation process that encodes an graph of objects describing a collection of compensating automata into a script that can be used with the LARVA runtime verification tool. We chose to target LARVA as it is the target with the highest level of abstraction that we could have made use of. We also managed to design a syntax with which to describe collections of compensating automata in a formal way. We chose to have a syntax that is base on that of LARVA's scripts so as to make the it easier to work with. We also implemented some test automata so as to check our translation procedure as well as a case study to gain more confidence in our implementation and in the compensating automata formalism itself. We also looked at other works that carry out some type of encoding of compensations into some kind of automaton or language and compared their approach with ours.