Verification of Artifact-Centric Systems: Decidability and Modeling Issues

  • Dmitry Solomakhin
  • Marco Montali
  • Sergio Tessaris
  • Riccardo De Masellis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8274)


Artifact-centric business processes have recently emerged as an approach in which processes are centred around the evolution of business entities, called artifacts, giving equal importance to control-flow and data. The recent Guard-State-Milestone (GSM) framework provides means for specifying business artifacts lifecycles in a declarative manner, using constructs that match how executive-level stakeholders think about their business. However, it turns out that formal verification of GSM is undecidable even for very simple propositional temporal properties. We attack this challenging problem by translating GSM into a well-studied formal framework.We exploit this translation to isolate an interesting class of “state-bounded” GSM models for which verification of sophisticated temporal properties is decidable. We then introduce some guidelines to turn an arbitrary GSM model into a state-bounded, verifiable model.


artifact-centric systems guard-stage-milestone formal verification 


  1. 1.
    van der Aalst, W.M.P., Stahl, C.: Modeling Business Processes - A Petri Net-Oriented Approach. Springer (2011)Google Scholar
  2. 2.
    Armando, A., Ponta, S.E.: Model checking of security-sensitive business processes. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 66–80. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Bagheri Hariri, B., Calvanese, D., De Giacomo, G., De Masellis, R., Felli, P., Montali, M.: Description logic knowledge and action bases. Journal of Artificial Intelligence Research, 651–686 (2013)Google Scholar
  4. 4.
    Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., Montali, M.: Verification of relational data-centric dynamic systems with external services. In: Proc. of PODS, pp. 163–174. ACM Press (2013)Google Scholar
  5. 5.
    Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proc. of KR. AAAI Press (2012)Google Scholar
  6. 6.
    Belardinelli, F., Lomuscio, A., Patrizi, F.: Verification of gsm-based artifact-centric systems through finite abstraction. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q. (eds.) ICSOC 2012. LNCS, vol. 7636, pp. 17–31. Springer, Heidelberg (2012)Google Scholar
  7. 7.
    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) (2007)Google Scholar
  8. 8.
    Calvanese, D., De Giacomo, G., Montali, M.: Foundations of data-aware process analysis: A database theory perspective. In: Proc. of PODS, pp. 1–12. ACM Press (2013)Google Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press (1999)Google Scholar
  10. 10.
    Cohn, D., Hull, R.: Business artifacts: A data-centric approach to modeling business operations and processes. IEEE Data Eng. Bull. 32(3) (2009)Google Scholar
  11. 11.
    Damaggio, E., Hull, R., Vaculin, R.: On the equivalence of incremental and fixpoint semantics for business artifacts with guard-stage-milestone lifecycles. Information Systems (2012)Google Scholar
  12. 12.
    Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proc. of ICDT, pp. 252–267. ACM Press (2009)Google Scholar
  13. 13.
    Dumas, M.: On the convergence of data and process engineering. In: Eder, J., Bielikova, M., Tjoa, A.M. (eds.) ADBIS 2011. LNCS, vol. 6909, pp. 19–26. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  14. 14.
    Emerson, E.A.: Model checking and the mu-calculus. In: Descriptive Complexity and Finite Models (1996)Google Scholar
  15. 15.
    Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verifying gsm-based business artifacts. In: Proc. of ICWS, pp. 25–32. IEEE (2012)Google Scholar
  16. 16.
    Group, T.O.M.: Object constraint language, version 2.0. Tech. Rep. formal/06-05-01, The Object Management Group (May 2006),
  17. 17.
    Morimoto, S.: A survey of formal verification for business process modeling. In: Bubak, M., van Albada, G.D., Dongarra, J., Sloot, P.M.A. (eds.) ICCS 2008, Part II. LNCS, vol. 5102, pp. 514–522. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    Nigam, A., Caswell, N.S.: Business artifacts: An approach to operational specification. IBM Systems Journal 42(3) (2003)Google Scholar
  19. 19.
    Puhlmann, F., Weske, M.: Using the pi-calculus for formalizing workflow patterns. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 153–168. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 20.
    Russo, A., Mecella, M., Montali, M., Patrizi, F.: Towards a reference implementation for data centric dynamic systems. In: Proc. of BPM Workshops (2013)Google Scholar
  21. 21.
    Solomakhin, D., Montali, M., Tessaris, S.: Formalizing guard-stage-milestone meta-models as data-centric dynamic systems. Tech. Rep. KRDB12-4, KRDB Research Centre, Faculty of Computer Science, Free University of Bozen-Bolzano (2012)Google Scholar
  22. 22.
    The Object Management Group: Case Management Model and Notation (CMMN), Beta 1 (January 2013),

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Dmitry Solomakhin
    • 1
  • Marco Montali
    • 1
  • Sergio Tessaris
    • 1
  • Riccardo De Masellis
    • 2
  1. 1.Free University of Bozen-BolzanoBolzanoItaly
  2. 2.Sapienza Università di RomaRomeItaly

Personalised recommendations