Modeling Long-Running Transactions with Communicating Hierarchical Timed Automata

Long-Running transactions consist of tasks which may be executed sequentially and in parallel, may contain sub-tasks, 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 Hierarchical Timed Automata suitable to describe the aspects mentioned. The automaton-theoretic approach allows the verification of properties by model checking. As a case study, we model and analyze an example of long

• Type: Conference
• Year: 2006
• Where: FMOODS
• Authors: Ruggero Lanotte, Andrea Maggiolo-Schettini, Paolo Milazzo, Angelo Troina
• Keywords: FMOODS 2006, FMOODS 2007, Hierarchical Timed Automata, Long-running Transactions, Model