This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Design and Verification of Long-Running Transactions with Extensible Coordination Tools
April-June 2013 (vol. 6 no. 2)
pp. 186-200
Farhad Arbab, CWI, Amsterdam
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.
Index Terms:
Business,Connectors,Light rail systems,Semantics,Automata,Integrated circuit modeling,Petri nets,verifiable design,Reo coordination language,long-running transactions,business process modeling
Citation:
Natallia Kokash, Farhad Arbab, "Formal Design and Verification of Long-Running Transactions with Extensible Coordination Tools," IEEE Transactions on Services Computing, vol. 6, no. 2, pp. 186-200, April-June 2013, doi:10.1109/TSC.2011.46
Usage of this product signifies your acceptance of the Terms of Use.