Formal modeling of BPEL workflows including fault and compensation handling

ABSTRACT

Electronically executed business processes are frequently implemented using the Business Process Execution Language (BPEL). These workflows may be in control of crucial business processes of an organization, in the same time existing model checking approaches are still immature i.e. they either seem to loose to much information during the generation of the analysis model, or the state space explosion prevents from model checking. We present a formal modeling technique for BPEL workflows including fault and compensation handling providing exact semantics with a state space size that allows for model checking. Additionally, error propagation among variables is supported so the effect of a faulty activity on the entire process can be examined.

REFERENCES

• 1: T. Andrews, F. Curbera, H. Dholakia, Y. Goland, J. Klein, F. Leymann, K. Liu, D. Roller, D. Smith, S. Thatte, I. Trickovic, and S. Weerawana. Business process execution language for web services version 1.1, 2003.
• 2: András Balogh , Dániel Varró, Advanced model transformation language constructs in the VIATRA2 framework, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France [doi>10.1145/1141277.1141575]
• 3: E. Christensen, F. Curbera, G. Meredith, and S. Weerawarana. Web services description language 1.1.
• 4: H. Foster. A Rigorous Approach To Engineering Web Service Composition. PhD thesis, Imperial College London, 2006.
• 5: J. García-Fanjul, J. Tuya, and C. de la Riva. Generating test cases specifications for compositions of web services. In A. Bertolino and A. Polini, editors, in Proceedings of International Workshop on Web Services Modeling and Testing (WS-MaTe2006), pages 83--94, Palermo, Sicily, ITALY, June 9th 2006.
• 6: S. Hinz, K. Schmidt, and C. Stahl. Transforming BPEL to Petri Nets. In W. M. P. v. d. Aalst, B. Benatallah, F. Casati, and F. Curbera, editors, Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, pages 220--235, Nancy, France, Sept. 2005. Springer-Verlag.
• 7: C. W. Ke Xu, Ying Liu. Bpsl modeler - visual notation language for intuitive business property reasoning. In GT-VMT, pages 205--214, 2006.
• 8: M. Kovács and L. Gönczy. Simulation and formal analysis of workflow models. In GT-VMT, pages 215--224, 2006.
• 9: S. Nakajima. Model-checking behavioral specification of bpel applications. Electr. Notes Theor. Comput. Sci., 151(2):89--105, 2006.
• 10: 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 ICSOC, pages 484--489, 2005.
• 11: K. Schmidt. Lola: A low level analyser. In ICATPN, pages 465--474, 2000.
• 12: Workflow management: models, methods, and systems, MIT Press, Cambridge, MA, 2002
• 13: Symbolic analysis laboratory. http://sal.csl.sri.com/.

INDEX TERMS

Keywords:
business process, compensation, fault modeling, model checking