\input zb-basic
\input zb-ioport
\iteman{io-port 05369878}
\itemau{Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Milazzo, Paolo; Troina, Angelo}
\itemti{Design and verification of long-running transactions in a timed framework.}
\itemso{Sci. Comput. Program. 73, No. 2-3, 76-94 (2008).}
\itemab
Summary: 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 automata-theoretic approach allows for the verification of properties by model checking. As a case study, we model and analyse an example of an e-commerce application described in terms of long-running transactions.
\itemrv{~}
\itemcc{}
\itemut{hierarchical timed automata; long-running transactions; compensations; model checking}
\itemli{doi:10.1016/j.scico.2008.07.001}
\end