Symbolic Abstraction and Deadlock-Freeness Verification of Inter-enterprise Processes

  • Kais Klai
  • Samir Tata
  • Jörg Desel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5701)


The design of complex inter-enterprise business processes (IEBP) is generally performed in a modular way. Each process is designed separately from the others and then the whole IEBP is obtained by composition. Even if such a modular approach is intuitive and facilitates the design problem, it poses the problem that correct behavior of each business process of the IEBP taken alone does not guarantee a correct behavior of the composed IEBP (i.e. properties are not preserved by composition). Proving correctness of the (unknown) composed process is strongly related to the model checking problem of a system model. Among others, the symbolic observation graph based approach has proven to be very helpful for efficient model checking in general. Since it is heavily based on abstraction techniques and thus hides detailed information about system components that are not relevant for the correctness decision, it is promising to transfer this concept to the problem rised in this paper: How can the symbolic observation graph technique be adapted and employed for process composition? Answering this question is the aim of this paper.


Business Process Label Transition System Reachability Graph Model Check Problem Dead State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Bultan, T., Su, J., Fu, X.: Analyzing conversations of web services. IEEE Internet Computing 10(1), 18–25 (2006)CrossRefGoogle Scholar
  3. 3.
    Dehnert, J., Rittgen, P.: Relaxed soundness of business processes. In: Dittrich, K.R., Geppert, A., Norrie, M.C. (eds.) CAiSE 2001. LNCS, vol. 2068, pp. 157–170. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Grefen, P., Aberer, K., Hoffner, Y., Ludwig, H.: Crossflow: Cross-organizational workflow management in dynamic virtual enterprises. International Journal of Computer Systems Science & Engineering 15(5), 277–290 (2000)Google Scholar
  5. 5.
    Grigori, D., Corrales, J.C., Bouzeghoub, M.: Behavioral matchmaking for service retrieval. In: ICWS 2006: Proceedings of the IEEE International Conference on Web Services, Washington, DC, USA, pp. 145–152. IEEE Computer Society Press, Los Alamitos (2006)CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Klai, K., Petrucci, L.: Modular construction of the symbolic observation graph. In: Billington, J., Duan, Z., Koutny, M. (eds.) ACSD, pp. 88–97. IEEE, Los Alamitos (2008)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting ws-bpel processes using flexible model generation. Data Knowl. Eng. 64(1), 38–54 (2008)CrossRefGoogle Scholar
  10. 10.
    Martens, A.: On Usability of Web Services. In: Calero, C., Daz, O., Piattini, M. (eds.) Proceedings of 1st Web Services Quality Workshop (WQW 2003), Rome, Italy (2003)Google Scholar
  11. 11.
    Martens, A.: Analyzing web service based business processes. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 19–33. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Martens, A.: Simulation and Equivalence between BPEL Process Models. In: Proceedings of the Design, Analysis, and Simulation of Distributed Systems Symposium (DASD 2005), Part of the 2005 Spring Simulation Multiconference (SpringSim 2005), San Diego, California (April 2005)Google Scholar
  13. 13.
    Martens, A., Simon, M., Achim, G., Karoline, F.: Analyzing compatibility of bpel processes. In: AICT-ICIW 2006: Proceedings of the Advanced Int’l Conference on Telecommunications and Int’l Conference on Internet and Web Applications and Services, Washington, DC, USA, p. 147. IEEE Computer Society Press, Los Alamitos (2006)Google Scholar
  14. 14.
    Massuthe, P., Wolf, K.: An Algorithm for Matching Nondeterministic Services with Operating Guidelines. Informatik-Berichte 202, Humboldt Universitat zu Berlin (2006)Google Scholar
  15. 15.
    Pankratius, V., Stucky, W.: A formal foundation for workflow composition, workflow view definition, and workflow normalization based on Petri nets. In: APCCM 2005: Proceedings of the 2nd Asia-Pacific conference on Conceptual modelling, Darlinghurst, Australia, Australia, pp. 79–88. Australian Computer Society, Inc. (2005)Google Scholar
  16. 16.
    Read, R., Corneil, D.: The Graph Isomorphism Disease. Graph Theory 1, 339–363 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    van der Aalst, W.M.P., Weske, M.: The P2P approach to interorganizational workflows. In: Dittrich, K.R., Geppert, A., Norrie, M.C. (eds.) CAiSE 2001. LNCS, vol. 2068, pp. 140–156. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    van Dijk, A.: Contracting workflows and protocol patterns. In: van der Aalst, W.M.P., ter Hofstede, A.H.M., Weske, M. (eds.) BPM 2003. LNCS, vol. 2678, pp. 152–167. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Kais Klai
    • 1
  • Samir Tata
    • 2
  • Jörg Desel
    • 3
  1. 1.LIPNCNRS UMR 7030, Université Paris 13VilletaneuseFrance
  2. 2.Institut TELECOMCNRS UMR SamovarEvryFrance
  3. 3.Department of Applied Computer ScienceCatholic University of Eichstätt-IngolstadtEichstättGermany

Personalised recommendations