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–running
transaction.