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. |
Year | DOI | Venue |
---|---|---|
2008 | 10.1016/j.scico.2008.07.001 | Sci. Comput. Program. |
Keywords | Field | DocType |
composition pattern,automaton-theoretic approach,model checking,compensation mechanism,long-running transactions,model checking.,compensations,long-running transaction,e-commerce application,case study,hierarchical timed automata,correct compensation,long-running transactions sequentially,communicating hierarchical timed automata,e commerce | Model checking,Programming language,Computer science,Automaton,Database transaction,Distributed computing | Journal |
Volume | Issue | ISSN |
73 | 2-3 | Science of Computer Programming |
Citations | PageRank | References |
15 | 0.73 | 49 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ruggero Lanotte | 1 | 257 | 28.31 |
Andrea Maggiolo-Schettini | 2 | 789 | 89.11 |
Paolo Milazzo | 3 | 328 | 21.14 |
Angelo Troina | 4 | 375 | 26.31 |