Ensuring transactional behavior of business processes and
web service compositions is an essential issue in the area of service-
oriented computing. Transactions in this context may require long peri-
ods of time to complete and must be managed using non-blocking tech-
niques. Compensations are activities executed to preserve data integrity
and eliminate the e®ects of a process terminated by a user or that failed
to complete due to another reason. This paper presents an approach to
formal modeling of long-running business transactions. Our solution is
based on the channel-based exogenous coordination language Reo, which
is an expressive, compositional and semantically precise design language
that admits formal reasoning. We illustrate how Reo can be used for
termination and compensation handling in a number of commonly-used
work°ow patterns, including sequential and parallel compositions, dis-
criminator choice and concurrent °ows with link dependencies.