Abstract
The Symbolic Observation Graph (SOG) associated with a labelled transition system and a subset of its labels is an efficient BDD-based abstraction representing the behavior of a system. The goal of this paper is to compose SOGs such that the resulting SOG is still small but represents the behavior of the composed business process in an appropriate way. In particular, we would like to deduce the properties of a composed business process by analysing the composition of the SOGs associated with its components. This question was already answered for the deadlock-freeness property in previous work. In this paper, we extend this result to other generic properties: the so-called soundness properties. These properties guarantee the absence of livelocks, deadlocks and other anomalies that can be formulated without domain knowledge. Thus, we show how the SOG can be adapted and used so that the verification of several variants of the soundness property can be performed modularly.
Chapter PDF
Similar content being viewed by others
References
van der Aalst, W.M.P.: Verification of Workflow Nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 407–426. Springer, Heidelberg (1997)
van der Aalst, W.M.P.: The application of Petri nets to workflow management. Journal of Circuits, Systems, and Computers 8(1), 21–66 (1998)
van der Aalst, W.M.P.: Loosely coupled interorganizational workflows: Modeling and analyzing workflows crossing organizational boundaries. Information and Management 37, 67–75 (2000)
van der Aalst, W.M.P.: Inheritance of interorganizational workflows: How to agree to disagree without loosing control? Information Technology and Management 4, 345–389 (2003)
Dehnert, J., Rittgen, P.: Relaxed Soundness of Business Processes. In: Dittrich, K.R., Geppert, A., Norrie, M. (eds.) CAiSE 2001. LNCS, vol. 2068, pp. 157–170. Springer, Heidelberg (2001)
Grigori, D., Corrales, J.C., Bouzeghoub, M.: Behavioral matchmaking for service retrieval. In: ICWS 2006: Proceedings of the IEEE International Conference on Web Services, pp. 145–152. IEEE (2006)
Haddad, S., Ilié, J.-M., Klai, K.: Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 196–210. Springer, Heidelberg (2004)
Klai, K., Ochi, H.: Modular verification of inter-enterprise business processes. In: The Fourth International Conference on Information, Process, and Knowledge Management, eKNOW 2012, pp. 155–161. IEEE (2012)
Klai, K., Petrucci, L.: Modular construction of the symbolic observation graph. In: ACSD, pp. 88–97. IEEE (2008)
Klai, K., Poitrenaud, D.: MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 288–306. Springer, Heidelberg (2008)
Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. Data Knowl. Eng. 70(5), 467–482 (2011)
Lohmann, N., Wolf, K.: Petrifying operating guidelines for services. In: ACSD, pp. 80–88. IEEE (2009)
Martens, A.: On compatibility of web services. Petri Net Newsletter, Special Interest Groups on Petri Nets and Related Systems Models, Gesellschaft fur Informatik e.V. 65, 12–20 (2003)
Martens, A.: On Usability of Web Services. In: Calero, C., Daz, O., Piattini, M. (eds.) Web Services Quality Workshop (2003)
Puhlmann, F., Weske, M.: Interaction Soundness for Service Orchestrations. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, pp. 302–313. Springer, Heidelberg (2006)
Siegeris, J., Zimmermann, A.: Workflow Model Compositions Preserving Relaxed Soundness. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 177–192. Springer, Heidelberg (2006)
van der Aalst, W.M.P., van Hee, K.M., van der Toorn, R.A.: Component-based software architectures: a framework based on inheritance of behavior. Sci. Comput. Program. 42(2-3), 129–171 (2002)
van Hee, K.M., Sidorova, N., Voorhoeve, M.: Soundness and Separability of Workflow Nets in the Stepwise Refinement Approach. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 337–356. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Klai, K., Desel, J. (2012). Checking Soundness of Business Processes Compositionally Using Symbolic Observation Graphs. In: Giese, H., Rosu, G. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2012 2012. Lecture Notes in Computer Science, vol 7273. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30793-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-30793-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30792-8
Online ISBN: 978-3-642-30793-5
eBook Packages: Computer ScienceComputer Science (R0)