Long-running transactions consist of tasks which may be executed sequentially and in parallel, may contain subtasks, and may require to be completed before a deadline. These transactions are not atomic and, in case of executions which cannot be completed, a compensation mechanism must be provided. In this paper we develop a model of Communicating Hierarchical Timed Automata suitable to describe the mentioned aspects in a framework where also time is taken into account. We develop the patterns for composing long-running transactions sequentially, in parallel or by nesting. The correct compensation of a composed long-running transaction is preserved by these composition patterns. The automaton-theoretic approach allows the verification of properties by model checking. As a case study, we model and analyse an example of e-commerce application described in terms of long-running transactions.
Design and Verification of Long-Running Transactions in a Timed Framework / R. Lanotte; A. Maggiolo-Schettini; P. Milazzo; A. Troina. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - STAMPA. - 73:(2008), pp. 76-94. [10.1016/j.scico.2008.07.001]
Design and Verification of Long-Running Transactions in a Timed Framework
TROINA, ANGELO
2008
Abstract
Long-running transactions consist of tasks which may be executed sequentially and in parallel, may contain subtasks, and may require to be completed before a deadline. These transactions are not atomic and, in case of executions which cannot be completed, a compensation mechanism must be provided. In this paper we develop a model of Communicating Hierarchical Timed Automata suitable to describe the mentioned aspects in a framework where also time is taken into account. We develop the patterns for composing long-running transactions sequentially, in parallel or by nesting. The correct compensation of a composed long-running transaction is preserved by these composition patterns. The automaton-theoretic approach allows the verification of properties by model checking. As a case study, we model and analyse an example of e-commerce application described in terms of long-running transactions.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.