Automatic Verification of Data-Centric Business Processes

  • Elio Damaggio
  • Alin Deutsch
  • Richard Hull
  • Victor Vianu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6896)


Recent years have witnessed the evolution of business process specification frameworks from the traditional process-centric approach towards data-awareness. Process-centric formalisms focus on control flow while under-specifying the underlying data and its manipulations by the process tasks, often abstracting them away completely. In contrast, data-aware formalisms treat data as first-class citizens. A notable exponent of this class is the business artifact model pioneered in [46, 34], deployed by IBM in professional services offerings with associated tooling, and further studied in a line of follow-up works [4, 5, 26, 27, 6, 38, 33, 35, 42]. Business artifacts (or simply “artifacts”) model key business-relevant entities, which are updated by a set of services that implement business process tasks. A collection of artifacts and services is called an artifact system. This modeling approach has been successfully deployed in practice, yielding proven savings when performing business process transformations [5, 4, 15].


Business Process Business Rule Shipment Type Artifact Model Arithmetic Constraint 
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.
    Abiteboul, S., Segoufin, L., Vianu, V.: Static analysis of active XML systems. ACM Trans. Database Syst. 34(4) (2009)Google Scholar
  2. 2.
    Abiteboul, S., Vianu, V., Fordham, B.S., Yesha, Y.: Relational transducers for electronic commerce. JCSS 61(2), 236–269 (2000), Extended abstract in PODS 1998zbMATHGoogle Scholar
  3. 3.
    Hariri, B.B., Calvanese, D., De Giacomo, G., De Masellis, R., Felli, P.: Foundations of relational artifacts verification. In: Rinderle, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 379–395. Springer, Heidelberg (2011)Google Scholar
  4. 4.
    Bhattacharya, K., Caswell, N.S., Kumaran, S., Nigam, A., Wu, F.Y.: Artifact-centered operational modeling: Lessons from customer engagements. IBM Systems Journal 46(4), 703–721 (2007)CrossRefGoogle Scholar
  5. 5.
    Bhattacharya, K., et al.: A model-driven approach to industrializing discovery processes in pharmaceutical research. IBM Systems Journal 44(1), 145–162 (2005)CrossRefGoogle Scholar
  6. 6.
    Bhattacharya, K., Gerede, C.E., Hull, R., Liu, R., Su, J.: Towards formal analysis of artifact-centric business process models. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 288–304. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS, pp. 7–16 (2006)Google Scholar
  8. 8.
    Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 1–22. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    Bouajjani, A., Habermehl, P., Mayr, R.: Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science 295, 85–106 (2003)CrossRefzbMATHGoogle Scholar
  10. 10.
    Bouajjani, A., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of infinite-state processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 690–705. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. 11.
    Bouyer, P.: A logical characterization of data languages. Information Processing Letters 84(2), 75–85 (2002)CrossRefzbMATHGoogle Scholar
  12. 12.
    Bouyer, P., Petit, A., Thérien, D.: An algebraic approach to data languages and timed languages. Information and Computation 182(2), 137–162 (2003)CrossRefzbMATHGoogle Scholar
  13. 13.
    Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification of infinite structures. In: Handbook of Process Algebra, pp. 545–623. Elsevier Science, Amsterdam (2001)CrossRefGoogle Scholar
  14. 14.
    Calvanese, D., De Giacomo, G., Hull, R., Su, J.: Artifact-centric workflow dominance. In: Baresi, L., Chi, C.-H., Suzuki, J. (eds.) ICSOC-ServiceWave 2009. LNCS, vol. 5900, pp. 130–143. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Chao, T., et al.: Artifact-based transformation of IBM Global Financing: A case study. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 261–277. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Damaggio, E., Deutsch, A., Vianu, V.: Artifact systems with data dependencies and arithmetic. In: Int’l. Conf. on Database Theory, ICDT (2011)Google Scholar
  17. 17.
    Damaggio, E., Hull, R., Vaculin, R.: On the equivalence of incremental and fixpoint semantics for business artifacts with guard-stage-milestone lifecycles. In: Rinderle, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 385–401. Springer, Heidelberg (2011)Google Scholar
  18. 18.
    de Man, H.: Case management: Cordys approach. BP Trends (February 2009),
  19. 19.
    Demri, S., Lazić, R.: LTL with the Freeze Quantifier and Register Automata. In: LICS, pp. 17–26 (2006)Google Scholar
  20. 20.
    Demri, S., Lazić, R., Sangnier, A.: Model checking freeze LTL over one-counter automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 490–504. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: ICDT, pp. 252–267 (2009)Google Scholar
  22. 22.
    Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. JCSS 73(3), 442–474 (2007)zbMATHGoogle Scholar
  23. 23.
    Deutsch, A., Sui, L., Vianu, V., Zhou, D.: A system for specification and verification of interactive, data-driven web applications. In: SIGMOD Conference (2006)Google Scholar
  24. 24.
    Dong, G., Hull, R., Kumar, B., Su, J., Zhou, G.: A framework for optimizing distributed workflow executions. In: Connor, R.C.H., Mendelzon, A.O. (eds.) DBPL 1999. LNCS, vol. 1949, pp. 152–167. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  25. 25.
    Hull, R., et al.: Introducing the guard-stage-milestone approach for specifying business entity lifecycles. In: Proc. of 7th Intl. Workshop on Web Services and Formal Methods, WS-FM, pp. 1–24 (2010)Google Scholar
  26. 26.
    Gerede, C.E., Bhattacharya, K., Su, J.: Static analysis of business artifact-centric operational models. In: IEEE International Conference on Service-Oriented Computing and Applications (2007)Google Scholar
  27. 27.
    Gerede, C.E., Su, J.: Specification and verification of artifact behaviors in business process models. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 181–192. Springer, Heidelberg (2007), CrossRefGoogle Scholar
  28. 28.
    Glushko, R.J., McGrath, T.: Document Engineering: Analyzing and Designing Documents for Business Informatics and Web Services. MIT Press, Cmabridge (2005)Google Scholar
  29. 29.
    Hull, R., Damaggio, E., De Masellis, R., Fournier, F., Gupta, M., Heath III, F., Hobson, S., Linehan, M., Maradugu, S., Nigam, A., Sukaviriya, P., Vaculín, R.: Business artifacts with guard-stage-milestone lifecycles: Managing artifact interactions with conditions and events. In: ACM Intl. Conf. on Distributed Event-based Systems, DEBS (2011)Google Scholar
  30. 30.
    Hull, R., Llirbat, F., Kumar, B., Zhou, G., Dong, G., Su, J.: Optimization techniques for data-intensive decision flows. In: Proc. IEEE Intl. Conf. on Data Engineering (ICDE), pp. 281–292 (2000)Google Scholar
  31. 31.
    Hull, R., Llirbat, F., Simon, E., Su, J., Dong, G., Kumar, B., Zhou, G.: Declarative workflows that support easy modification and dynamic browsing. In: Proc. Int. Joint Conf. on Work Activities Coordination and Collaboration (1999)Google Scholar
  32. 32.
    Jurdzinski, M., Lazić, R.: Alternation-free modal mu-calculus for data trees. In: LICS, pp. 131–140 (2007)Google Scholar
  33. 33.
    Kumaran, S., Liu, R., Wu, F.Y.: On the duality of information-centric and activity-centric models of business processes. In: Bellahsène, Z., Léonard, M. (eds.) CAiSE 2008. LNCS, vol. 5074, pp. 32–47. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  34. 34.
    Kumaran, S., Nandi, P., Heath, T., Bhaskaran, K., Das, R.: ADoc-oriented programming. In: Symp. on Applications and the Internet (SAINT), pp. 334–343 (2003)Google Scholar
  35. 35.
    Küster, J., Ryndina, K., Gall, H.: Generation of BPM for object life cycle compliance. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 165–181. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  36. 36.
    Lazić, R., Newcomb, T., Ouaknine, J., Roscoe, A., Worrell, J.: Nets with tokens which carry data. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 301–320. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  37. 37.
    Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)CrossRefzbMATHGoogle Scholar
  38. 38.
    Liu, R., Bhattacharya, K., Wu, F.Y.: Modeling business contexture and behavior using business artifacts. In: Krogstie, J., Opdahl, A.L., Sindre, G. (eds.) CAiSE 2007 and WES 2007. LNCS, vol. 4495, pp. 324–339. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  39. 39.
    Martin, D., et al.: OWL-S: Semantic markup for web services, W3C Member Submission (November 2003)Google Scholar
  40. 40.
    McIlraith, S.A., Son, T.C., Zeng, H.: Semantic web services. IEEE Intelligent Systems 16(2), 46–53 (2001)CrossRefGoogle Scholar
  41. 41.
    Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River (1967)zbMATHGoogle Scholar
  42. 42.
    Nandi, P., et al.: Data4BPM, Part 1: Introducing Business Entities and the Business Entity Definition Language (BEDL) (April 2010),
  43. 43.
    Nandi, P., Kumaran, S.: Adaptive business objects – a new component model for business integration. In: Proc. Intl. Conf. on Enterprise Information Systems, pp. 179–188 (2005)Google Scholar
  44. 44.
    Narayanan, S., McIlraith, S.: Simulation, verification and automated composition of web services. In: Intl. World Wide Web Conf, (WWW 2002) (2002)Google Scholar
  45. 45.
    Neven, F., Schwentick, T., Vianu, V.: Finite State Machines for Strings Over Infinite Alphabets. ACM Transactions on Computational Logic 5(3), 403–435 (2004)CrossRefGoogle Scholar
  46. 46.
    Nigam, A., Caswell, N.S.: Business artifacts: An approach to operational specification. IBM Systems Journal 42(3), 428–445 (2003)CrossRefGoogle Scholar
  47. 47.
    Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)Google Scholar
  48. 48.
    Segoufin, L., Torunczyk, S.: Automata based verification over linearly ordered data domains. In: Int’l. Symp. on Theoretical Aspects of Computer Science, STACS (2011)Google Scholar
  49. 49.
    Spielmann, M.: Verification of relational transducers for electronic commerce. JCSS 66(1), 40–65 (2003), Extended abstract in PODS 2000zbMATHGoogle Scholar
  50. 50.
    Wang, J., Kumar, A.: A framework for document-driven workflow systems. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 285–301. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  51. 51.
    Zhao, X., Su, J., Yang, H., Qiu, Z.: Enforcing constraints on life cycles of business artifacts. In: TASE, pp. 111–118 (2009)Google Scholar
  52. 52.
    Zhu, W.-D., et al.: Advanced Case Management with IBM Case Manager. Published by IBM,

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Elio Damaggio
    • 1
  • Alin Deutsch
    • 1
  • Richard Hull
    • 2
  • Victor Vianu
    • 1
  1. 1.University of CaliforniaSan DiegoUSA
  2. 2.IBM T.J. Watson Research CenterUSA

Personalised recommendations