Implementing rigorous web services with process algebra: navigation plan for web services

ABSTRACT

Despite the popularity of standards such as BPEL in business-critical applications, rigorous approaches to web service composition remain an open research problem. Frameworks based on formal foundations (e.g., process algebra or Petri nets) have emerged as promising approach to address these challenges. This work introduces the Navigation Plan for Web Services (NPWS), a system module, which extends a process algebra based workflow engine with a web service interface. We systematically combine the web service paradigm and comprehensive real-world workflow functionality while guaranteeing sound properties through formal process specification. Process instantiation and execution monitoring are implemented with Enterprise JavaBeans, SQL extension, and Java Persistence API to ensure flexibility and scalable integration. Our primary contribution is an applied approach to implementing complex web services with formal properties through a well-defined process algebraic core. We further illustrate our system with sample client applications and a case study based on an actual deployment in a library environment.

REFERENCES

• 1: jBPM. http://www.jboss.org/jbossjbpm, July 2008.
• 2: Kelly Rosa Braghetto , João Eduardo Ferreira , Calton Pu, Using control-flow patterns for specifying business processes in cooperative environments, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea [doi>10.1145/1244002.1244270]
• 3: K. R. Braghetto, J. E. Ferreira, and C. Pu. Business processes management using process algebra and relational database model. In ICE-B, 2008.
• 4: D. Fahland and W. Reisig. ASM-based semantics for BPEL: The negative control flow. In Abstract State Machines, pages 131--152, 2005.
• 5: Andrea Ferrara, Web services: a process algebra approach, Proceedings of the 2nd international conference on Service oriented computing, November 15-19, 2004, New York, NY, USA [doi>10.1145/1035167.1035202]
• 6: Joao Eduardo Ferreira , Osvaldo K. Takai , Kelly R. Braghetto , Calton Pu, Large Scale Order Processing through Navigation Plan Concept, Proceedings of the IEEE International Conference on Services Computing, p.297-300, September 18-22, 2006 [doi>10.1109/SCC.2006.62]
• 7: J. E. Ferreira, O. K. Takai, and C. Pu. Integration of collaborative information system in internet applications using riverfish architecture. In CollaborateCom. IEEE, 2005.
• 8: J. A. Fisteus, L. S. Fernández, and C. D. Kloos. Formal verification of BPEL4WS business collaborations. E-Commerce and Web Technologies, pages 76--85, 2004.
• 9: Wan Fokkink , W. Brauer , G. Rozenberg , A. Salomaa, Introduction to Process Algebra, Springer-Verlag New York, Inc., Secaucus, NJ, 2000
• 10: Richard Hull , Jianwen Su, Tools for design of composite Web services, Proceedings of the 2004 ACM SIGMOD international conference on Management of data, June 13-18, 2004, Paris, France [doi>10.1145/1007568.1007722]
• 11: D. Jordan and J. Evdemon. Web services business process execution language version 2.0. Public Review Draft OASIS WS-BPEL Technical Committee, April 2007.
• 12: N. Kavantzas, D. Burdett, G. Ritzinger, T. Fletcher, Y. Lafon, and C. Barreto. Web services choreography description language version 1.0. W3C Candidate Recommendation, November 2005.
• 13: C. Ouyang, E. Verbeek, W. M. P. van der Aalst, S. Breutel, M. Dumas, and A. H. M. ter Hofstede. WofBPEL: A tool for automated analysis of BPEL processes. In B. Benatallah, F. Casati, and P. Traverso, editors, ICSOC, volume 3826 of Lecture Notes in Computer Science, pages 484--489. Springer, 2005.
• 14: F. Puhlmann and M. Weske. Using the π-calculus for formalizing workflow patterns. Business Process Management, pages 153--168, 2005.
• 15: Hajo A. Reijers, Workflow Flexibility: The Forlorn Promise, Proceedings of the 15th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises, p.271-272, June 26-28, 2006 [doi>10.1109/WETICE.2006.80]
• 16: Maurice ter Beek , Antonio Bucchiarone , Stefania Gnesi, Web Service Composition Approaches: From Industrial Standards to Formal Methods, Proceedings of the Second International Conference on Internet and Web Applications and Services, p.15, May 13-19, 2007 [doi>10.1109/ICIW.2007.71]
• 17: F. van Breugel and M. Koshkina. Models and verification of BPEL. Unpublished Draft, September 2006. http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf.
• 18: Wil M. P. van der Aalst, Verification of Workflow Nets, Proceedings of the 18th International Conference on Application and Theory of Petri Nets, p.407-426, June 23-27, 1997
• 19: W. M. P. van der Aalst. The application of petri nets to workflow management. Journal of Circuits, Systems, and Computers, 8(1): 21--66, 1998.
• 20: Wil M. P. van der Aalst , Marlon Dumas , Arthur H. M. ter Hofstede, Web Service Composition Languages: Old Wine in New Bottles?, Proceedings of the 29th Conference on EUROMICRO, p.298, September 01-06, 2003
• 21: W. M. P. van der Aalst , A. H. M. ter Hofstede, YAWL: yet another workflow language, Information Systems, v.30 n.4, p.245-275, June 2005 [doi>10.1016/j.is.2004.02.002]
• 22: W. M. P. Van Der Aalst , A. H. M. Ter Hofstede , B. Kiepuszewski , A. P. Barros, Workflow Patterns, Distributed and Parallel Databases, v.14 n.1, p.5-51, July 2003 [doi>10.1023/A:1022883727209]
• 23: Mathias Weske, Business Process Management: Concepts, Languages, Architectures, Springer-Verlag New York, Inc., Secaucus, NJ, 2007

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.5 On-line Information Services
          Subjects: Web-based services

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Algebraic language theory

General Terms:
Design, Documentation, Verification

Keywords:
BPEL, implementation, process algebra, software, web services, workflow