Abstract
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.
Chapter PDF
Similar content being viewed by others
References
van der Aalst, W.M.P., Stahl, C.: Modeling Business Processes - A Petri Net-Oriented Approach. Springer (2011)
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)
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)
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)
Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proc. of KR. AAAI Press (2012)
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)
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)
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)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press (1999)
Cohn, D., Hull, R.: Business artifacts: A data-centric approach to modeling business operations and processes. IEEE Data Eng. Bull. 32(3) (2009)
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)
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)
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)
Emerson, E.A.: Model checking and the mu-calculus. In: Descriptive Complexity and Finite Models (1996)
Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verifying gsm-based business artifacts. In: Proc. of ICWS, pp. 25–32. IEEE (2012)
Group, T.O.M.: Object constraint language, version 2.0. Tech. Rep. formal/06-05-01, The Object Management Group (May 2006), http://www.omg.org/spec/OCL/2.0/
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)
Nigam, A., Caswell, N.S.: Business artifacts: An approach to operational specification. IBM Systems Journal 42(3) (2003)
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)
Russo, A., Mecella, M., Montali, M., Patrizi, F.: Towards a reference implementation for data centric dynamic systems. In: Proc. of BPM Workshops (2013)
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)
The Object Management Group: Case Management Model and Notation (CMMN), Beta 1 (January 2013), http://www.omg.org/spec/CMMN/1.0/Beta1/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Solomakhin, D., Montali, M., Tessaris, S., De Masellis, R. (2013). Verification of Artifact-Centric Systems: Decidability and Modeling Issues. In: Basu, S., Pautasso, C., Zhang, L., Fu, X. (eds) Service-Oriented Computing. ICSOC 2013. Lecture Notes in Computer Science, vol 8274. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45005-1_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-45005-1_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45004-4
Online ISBN: 978-3-642-45005-1
eBook Packages: Computer ScienceComputer Science (R0)