Abstract
We survey the use of the Abstract State Machines (ASM) method for a rigorous foundation of modeling and validating web services, workflows, interaction patterns and business processes. We show in particular that one can tailor business process definitions in application-domain yet rigorous terms in such a way that the resulting ASM models can be used as basis for binding contracts between domain experts and IT technologists. The method combines the expressive power and accuracy of rule-based modeling with the intuition provided by visual graph-based descriptions. We illustrate this by an ASM-based semantical framework for the OMG standard for BPMN (Business Process Modeling Notation). The framework supports true concurrency, heterogeneous state and modularity (compositional design and verification techniques). As validation example we report some experiments, carried out with a special-purpose ASM simulator, to evaluate various definitions proposed in the literature for the critical OR-join construct of BPMN.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barros, A., Dumas, M., Hofstede, A.: Service interaction patterns. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 302–318. Springer, Heidelberg (2005)
Altenhofen, M., Börger, E., Friesen, A., Lemcke, J.: A high-level specification for virtual providers. International Journal of Business Process Integration and Management 1(4), 267–278 (2006)
Altenhofen, M., Börger, E., Lemcke, J.: A high-level specification for mediators (virtual providers). In: Bussler, C.J., Haller, A. (eds.) BPM 2005. LNCS, vol. 3812, pp. 116–129. Springer, Heidelberg (2006)
Altenhofen, M., Friesen, A., Lemcke, J.: ASMs in service oriented architectures. Journal of Universal Computer Science (2008)
Barros, A., Börger, E.: A compositional framework for service interaction patterns and communication flows. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 5–35. Springer, Heidelberg (2005)
Batory, D., Börger, E.: Modularizing theorems for software product lines: The Jbook case study. In: Hartmann, S., Kern-Isberner, G. (eds.) FoIKS 2008. LNCS, vol. 4932, pp. 1–4. Springer, Heidelberg (2008)
Batory, D., O’Malley, S.: The design and implementation of hierarchical software systems with reusable components. In: ACM TOSEM. ASM (October 1992)
Börger, E.: The ASM refinement method. Formal Aspects of Computing 15, 237–257 (2003)
Börger, E.: Construction and analysis of ground models and their refinements as a foundation for validating computer based systems. Formal Aspects of Computing 19, 225–241 (2007)
Börger, E.: Modeling workflow patterns from first principles. In: Storey, V.C., Parent, C., Schewe, K.-D., Thalheim, B. (eds.) ER 2007. LNCS, vol. 4801, pp. 1–20. Springer, Heidelberg (2007)
Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Börger, E., Thalheim, B.: Experiments with the behavior of or-joins in business process models. J. Universal Computer Science (submitted, 2008)
Börger, E., Thalheim, B.: A high-level BPMN interpreter (submitted)
Börger, E., Thalheim, B.: A method for verifiable and validatable business process modeling. In: Advances in Software Engineering. LNCS, Springer, Heidelberg (2008)
BPMI.org. Business Process Modeling Notation Specification. dtc/2006-02-01 (2006), http://www.omg.org/technology/documents/spec_catalog.htm
Dijkman, R.M., Dumas, M., Ouyang, C.: Formal semantics and analysis of BPMN process models using Petri nets. Technical Report 7115, Queensland University of Technology, Brisbane (2007)
Fahland, D.: Ein Ansatz einer Formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines. Master’s thesis, Humboldt-Universität zu Berlin (June 2004)
Fahland, D., Reisig, W.: ASM semantics for BPEL: the negative control flow. In: Beauquier, D., Börger, E., Slissenko, A. (eds.) Proc. ASM 2005, Université de Paris, vol. 12, pp. 131–152 (2005)
Farahbod, R., Glässer, U., Vajihollahi, M.: Specification and validation of the Business Process Execution Language for web services. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 78–94. Springer, Heidelberg (2004)
Friesen, A., Börger, E.: A high-level specification for semantic web service discovery services. In: ICWE 2006: Workshop Proceedings of the Sixth International Conference on Web Engineering (2006)
Lavagno, L., Sangiovanni-Vincentelli, A., Sentovitch, E.M.: Models of computation for system design. In: Börger, E. (ed.) Architecture Design and Validation Methods, pp. 243–295. Springer, Heidelberg (2000)
Lemcke, J., Friesen, A.: Composing web-service-like Abstract State Machines (ASMs). In: Workshop on Web Service Composition and Adaptation (WSCA 2007); IEEE International Conference on Web Service (ICWS 2007) (2007)
Farahbod, U.G.R., Vajihollahi, M.: An Abstract Machine Architecture for Web Service Based Business Process Management. Int. J. Business Process Integration and Management 1(4), 279–291 (2006)
Russel, N., ter Hofstede, A., van der Aalst, W.M.P., Mulyar, N.: Workflow control-flow patterns: A revised view. BPM-06-22 (July 2006), http://is.tm.tue.nl/staff/wvdaalst/BPMcenter/
Sörensen, O.: Diplomarbeit. Master’s thesis, University of Kiel, forthcoming (2008), www.is.informatik.uni-kiel/ thalheim/ASM/MetaProgrammingASM
Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)
van der Aalst, W., ter Hofstede, A., Kiepuszewski, B., Barros, A.: Workflow patterns. Distributed and Parallel Databases 14(3), 5–51 (2003)
Weske, M.: Business Process Management. Springer, Heidelberg (2007)
Wohed, P., van der Aalst, W.M.P., Dumas, M., ter Hofstede, A., Russel, N.: On the suitability of BPMN for business process modelling. In: The 4th Int. Conf. on Business Process Management (2006)
Wong, P.Y.H., Gibbons, J.: A process semantics fo BPMN. Oxford University Computing Lab (preprint, July 2007), http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/bpmn_extended.pdf
Wynn, M., van der Aalst, W., ter Hofstede, A., Edmond, D.: Verifying workflows with cancellation regions and OR-joins: an approach based on reset nets and reachability analysis. In: Dustdar, S., Fiadeiro, J.L., Seth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 389–394. Springer, Heidelberg (2006); Previous versions edited as BPM-06-16 and BPM-06-12
Wynn, M., Verbeek, H.M.W., van der Aalst, W., ter Hofstede, A., Edmond, D.: Reduction rules for reset workflow nets. Technical Report BPM-06-25, BPMcenter.org (2006)
Wynn, M., Verbeek, H.M.W., van der Aalst, W., ter Hofstede, A., Edmond, D.: Reduction rules for YAWL workflow nets with cancellation regions and OR-joins. Technical Report BPM-06-24, BPMcenter.org (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Börger, E., Thalheim, B. (2008). Modeling Workflows, Interaction Patterns, Web Services and Business Processes: The ASM-Based Approach. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds) Abstract State Machines, B and Z. ABZ 2008. Lecture Notes in Computer Science, vol 5238. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87603-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-87603-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87602-1
Online ISBN: 978-3-540-87603-8
eBook Packages: Computer ScienceComputer Science (R0)