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 periods of time to complete and must be managed using nonblocking techniques. Data integrity in long-running transactions (LRTs) is preserved using compensations, that is, activities explicitly programmed to eliminate the effects of a process terminated by a user or that failed to complete due to another reason. In this paper, we present a framework for behavioral modeling of business processes, focusing on their transactional properties. Our solution is based on the channel-based coordination language Reo, which is an expressive, compositional, and semantically precise design language admitting formal reasoning. The operational semantics of Reo is given by constraint automata (CA). We illustrate how Reo can be used for modeling termination and compensation handling in a number of commonly used workflow patterns, including sequential and parallel compositions, nested transactions, discriminator choice and concurrent flows with link dependences. Furthermore, we show how essential properties of LRTs can be expressed in LTL and CTL-like logics and verified using model checking technology. Our framework is supported by a number of Eclipse plug-ins that provides facilities for modeling, animation, and verification of LRTs to generate executable code for them.

Abstract The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints imposed by connectors. To ensure that the composed system behaves as intended, we need a wide range of automated verification tools to assist service composition designers. In this paper, we present our framework for the verification of Reo using the mCRL2 toolset. We unify our previous work on mapping various semantic models for Reo, namely, constraint automata, timed constraint automata, coloring semantics and the newly developed action constraint automata, to the process algebraic specification language of mCRL2, address the correctness of this mapping, discuss tool support, and present a detailed example that illustrates the use of Reo empowered with mCRL2 for the analysis of dataflow in service-based process models.

Reo is a graphical channel-based coordination language that enables the modeling of complex behavioral protocols using a small set of channel types with well-de ned behavior. Reo has been developed for the coordination of standalone components and services, which makes it suitable for the modeling of service-based business processes. The formal semantic models for Reo lay the grounds for computer-aided analysis of different aspects of Reo diagrams, including their animation, simulation and veri cation of control ow and data ow by means of model checking techniques. In this paper, we discuss the veri cation of data aware Reo process models using the mCRL2 model checking toolset including time analysis. We also show how behavior abstraction can be used to minimize Reo process models and generate smaller mCRL2 speci cations. A detailed auction example illustrates our approach to timeaware modeling and veri cation of data-centric service models.