Modeling long-running transactions with communicating hierarchical timed automata