The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - April-June (2013 vol.6)
pp: 186-200
Farhad Arbab , CWI, Amsterdam
ABSTRACT
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
REFERENCES
[1] N. Kokash and F. Arbab, "Applying Reo to Service Coordination in Long-Running Business Transactions," Proc. ACM Symp. Applied Computing (SAC '09), pp. 318-319, 2009.
[2] A. Lazovik and F. Arbab, "Using Reo for Service Coordination," Proc. Fifth Int'l Conf. Service-Oriented Computing (ICSOC '07), vol. 4749, pp. 398-403, 2007.
[3] F. Arbab, "A Behavioral Model for Composition of Software Components," Proc. L'Objet: Selected Papers of the Int'l Workshop Coordination and Adaptation of Software Entities (WCAT '04), vol. 12, no. 1, pp. 33-76, 2006.
[4] F. Arbab, N. Kokash, and M. Sun, "Towards Using Reo for Compliance-Aware Business Process Modelling," Proc. Leveraging Applications of Formal Methods Conf. (ISoLA '08), vol. 17, 2008.
[5] L. Bocchi, C. Laneve, and G. Zavattaro, "A Calculus for Long-Running Transactions," Formal Methods for Open Object-Based Distributed Systems, vol. 2884, pp. 124-138, 2003.
[6] L. Bocchi, "Compositional Nested Long-Running Transactions," Proc. Fundamental Approaches to Software Eng. Conf. (FASE '04), vol. 2984, pp. 194-208, 2004.
[7] M. Butler and C. Ferreira, "An Operational Semantics for StAC, A Language for Modelling Long-Running Business Transactions," Coordination Models and Languages, vol. 2949, pp. 87-104, 2004.
[8] M. Butler, T. Hoare, and C. Ferreira, "A Trace Semantics for Long-Running Transactions," Proc. Communicating Sequential Processes, vol. 3525, pp. 133-150, 2005.
[9] R. Bruni, H. Melgratti, and U. Montanari, "Theoretical Foundations for Compensations in Flow Composition Languages," Proc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, vol. 40, no. 1, pp. 209-220, 2005.
[10] R. Bruni, M.J. Butler, C. Ferreira, C.A.R. Hoare, H.C. Melgratti, and U. Montanari, "Comparing Two Approaches to Compensable Flow Composition," Proc. Int'l Conf. Concurrency Theory (CONCUR '05), vol. 3653, pp. 383-397, 2005.
[11] W. Gaaloul, M. Rouached, C. Godart, and M. Hauswirth, "Verifying Composite Service Transactional Behavior Using Event Calculus," Proc. OTM Confederated Int'l Conf. the Move to Meaningful Internet Systems: CoopIS, DOA, ODBASE, GADA, and IS, vol. 4803, pp. 353-370, 2007.
[12] O.P.S. Bhiri and C. Godart, "Transactional Patterns for Reliable Web Services Compositions," Proc. Int'l Conf. Web Eng. (ICWE '06), pp. 137-144, 2006.
[13] R. Lucchi and M. Mazzara, "A Pi-Calculus Based Semantics for WS-BPEL," J. Logic and Algebraic Programming, vol. 70, no. 1, pp. 96-118, 2007.
[14] C. Laneve and G. Zavattaro, "Foundations of Web Transactions," Proc. Eighth Int'l Conf. Foundations of Software Science and Computation Structures (FOSSACS '05), vol. 3441, pp. 282-298, 2005.
[15] G. Pu, H. Zhu, Z. Qiu, S. Wang, X. Zhao, and J. He, "Theoretical Foundations of Scope-Based Compensable Flow Language for Web Service," Proc. Eighth IFIP WG 6.1 Int'l Conf. Formal Methods for Open Object-Based Distributed Systems (FMOODS '06), vol. 4037, pp. 251-266, 2006.
[16] C. Eisentraut and D. Spieler, "Failure, Compensation and Termination in BPEL 2.0 A Comparative Analysis," Proc. Int'l Workshop Web Services and Formal Methods, 2008.
[17] N. Lohmann, "A Feature-Complete Petri Net Semantics for WS-BPEL 2.0," Proc. Int'l Workshop Web Services and Formal Methods, vol. 4937, pp. 77-91, 2008.
[18] T. Takemura, "Formal Semantics and Verification of BPMN Transaction and Compensation," Proc. IEEE Asia-Pacific Services Computing Conf., pp. 284-290, 2008.
[19] I. Raedts, M. Petković, Y.S. Usenko, J.M. van der Werf, J.F. Groote, and L. Somers, "Transformation of BPMN Models for Behaviour Analysis," Proc. Int'l Workshop Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS '07), pp. 126-137, 2007.
[20] R. Lanotte, A. Maggiolo-Schettini, P. Milazzo, and A. Troina, "Design and Verification of Long-Running Transactions in a Timed Framework," Science of Computer Programming, vol. 73, nos. 2/3, pp. 76-94, 2008.
[21] OMG, "Business Process Modeling Notation (BPMN) Specification," http://www.omg.org/bpmn/DocumentsOMG_Final_ Adopted_BPMN_1-0_Spec_06-02-01.pdf , Final Adopted Specification, 2006.
[22] A. Alves et al., "Web Services Business Process Execution Language (WS-BPEL) Version 2.0," OASIS, http://docs.oasis-open.org/wsbpel/2.0wsbpel-specification-draft.pdf , Public Rev. Draft, 2006.
[23] W. Cox, F. Cabrera, G. Copeland, T. Freund, J. Klein, T. Storey, and S. Thatte, "Web Services Transaction (WS-Transaction)," technical report, BEA, IBM and Microsoft, http://dev2dev.bea. com/pub/a/2004/01ws-transaction.html , 2004.
[24] J. Gray and A. Reuter, Transaction Processing: Concepts and Techniques, Morgan Kaufmann, 1993.
[25] F. Arbab, "Reo: A Channel-Based Coordination Model for Component Composition," Math. Structures in Computer Science, vol. 14, no. 3, pp. 329-366, 2004.
[26] F. Arbab, C. Baier, F.S. de Boer, and J.J.M.M. Rutten, "Models and Temporal Logics for Timed Component Connectors," Int'l J. Software and Systems Modeling, vol. 6, no. 1, pp. 59-82, 2007.
[27] C. Baier, "Probabilistic Models for Reo Connector Circuits," J. Universal Computer Science, vol. 11, no. 10, pp. 1718-1748, 2005.
[28] F. Arbab, T. Chothia, R. van der Mei, S. Meng, Y.-J. Moon, and C. Verhoef, "From Coordination to Stochastic Models of QoS," Proc. 11th Int'l Conf. Coordination Models and Languages (COORDINATION '09), vol. 5521, pp. 268-287, 2009.
[29] S. Sadiq, G. Governatori, and K. Naimiri, "Modeling Control Objectives for Business Process Compliance," Proc. Fifth Int'l Conf. Business Process Management (BPM '07), vol. 4714, pp. 149-164, 2007.
[30] C. Baier, M. Sirjani, F. Arbab, and J. Rutten, "Modeling Component Connectors in Reo by Constraint Automata," Science of Computer Programming, vol. 61, pp. 75-113, 2006.
[31] D. Clarke, D. Costa, and F. Arbab, "Connector Coloring I: Synchronization and Context Dependency," Science of Computer Programming, vol. 66, pp. 205-225, 2007.
[32] N. Kokash, B. Changizi, and F. Arbab, "A Semantic Model for Service Composition with Coordination Time Delays," Proc. 12th Int'l Conf. Formal Eng. Methods and Software Eng. (ICFEM '10), pp. 106-121, 2010.
[33] N. Kokash, C. Krause, and E. de Vink, "Data-Aware Design and Verification of Service Composition with Reo and mCRL2," Proc. ACM Symp. Applied Computing (SAC '10), pp. 2406-2413, 2010.
[34] N. Kokash, C. Krause, and E. de Vink, "Verification of Context-Dependent Channel-Based Service Models," Proc. Int'l Conf. Formal Methods for Components and Objects (FMCO '10), vol. 6286, pp. 21-40, 2010.
[35] J. Groote, A. Mathijssen, M. Reniers, Y. Usenko, and M. van Weerdenburg, "The Formal Specification Language mCRL2," Proc. Methods for Modelling Software Systems. Dagstuhl Seminar, 2007.
[36] N. Kokash, C. Krause, and E. de Vink, "Time and Data Aware Analysis of Graphical Service Models in Reo," Proc. IEEE Eighth Int'l Conf. Software Eng. and Formal Methods (SEFM '10), pp. 125-134, 2010.
[37] C. Baier, T. Blechmann, J. Klein, and S. Klüppelholz, "A Uniform Framework for Modeling and Verifying Components and Connectors," Proc. 11th Int'l Conf. Coordination Models and Languages (COORDINATION '09), vol. 5521, pp. 268-287, 2009.
[38] J.C.M. Dwyer and G. Avrunin, "Property Specification Patterns for Finite-State Verification," Proc. Int'l Workshop Formal Methods on Software Practice, pp. 7-15, 1998.
[39] R. Alur and D. Dill, "A Theory of Timed Automata," Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.
[40] S. Kemper, "SAT-Based Verification for Timed Component Connectors," Electronic Notes in Theoretical Computer Science, vol. 255, pp. 103-118, 2009.
[41] F. Jouault, F. Allilaire, J. Tezivin, I. Kurtev, and P. Valduriez, "ATL: A QVT-Like Transformation Language," Proc. 21st ACM SIGPLAN Symp. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '06), pp. 719-720, 2006.
[42] B. Changizi, N. Kokash, and F. Arbab, "A Unified Toolset for Business Process Model Formalization," Proc. Int'l Workshop Formal Eng. Approaches to Software Components and Architectures (FESCA '10), pp. 147-156, 2010.
36 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool