Verification of Deployed Artifact Systems via Data Abstraction

  • Francesco Belardinelli
  • Alessio Lomuscio
  • Fabio Patrizi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7084)


Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycle models, accounting for the relational structure of the artifact state and its possible evolutions over time. We consider the problem of verifying artifact systems against specifications expressed in quantified temporal logic. This problem is in general undecidable. However, when artifact systems are deployed, their states can contain only a bounded number of elements. We exploit this fact to develop an abstraction technique that enables us to verify deployed artifact systems by model checking their bounded abstraction.


Business Process Model Check Data Abstraction Database Schema Kripke Structure 
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.


  1. 1.
    Bagheri Hariri, B., Calvanese, D., De Giacomo, G., De Masellis, R., Felli, P.: Foundations of Relational Artifacts Verification. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 379–395. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Belardinelli, F., Lomuscio, A., Patrizi, F.: A Computationally-Grounded Semantics for Artifact-Centric Systems and Abstraction Results. In: Proc. of IJCAI (to appear, 2011)Google Scholar
  3. 3.
    Berardi, D., Calvanese, D., De Giacomo, G., Hull, R., Mecella, M.: Automatic Composition of Transition-based Semantic Web Services with Messaging. In: Proc. of VLDB (2005)Google Scholar
  4. 4.
    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
  5. 5.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers 58, 118–149 (2003)Google Scholar
  6. 6.
    Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Caucal, D.: On Infinite Transition Graphs having a Decidable Monadic Theory. Theoretical Computer Science 290(1), 79–115 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (2000)Google Scholar
  9. 9.
    Cohn, D., Hull, R.: Business Artifacts: A Data-Centric Approach to Modeling Business Operations and Processes. IEEE Data Eng. Bull. 32(3), 3–9 (2009)Google Scholar
  10. 10.
    Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic Verification of Data-centric Business Processes. In: Proc. of ICDT (2009)Google Scholar
  11. 11.
    Deutsch, A., Sui, L., Vianu, V.: Specification and Verification of Data-Driven Web Applications. J. Comput. Syst. Sci. 73(3), 442–474 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic, vol. 148. Elsevier (2003)Google Scholar
  13. 13.
    Hull, R., Damaggio, E., De Masellis, R., Fournier, F., Gupta, M., Heath III, F.T., Hobson, S., Linehan, M.H., Maradugu, S., Nigam, A., Sukaviriya, P., Vaculín, R.: Business Artifacts with Guard-Stage-Milestone Lifecycles: Managing Artifact Interactions with Conditions and Events. In: Proc. of DEBS (to appear, 2011)Google Scholar
  14. 14.
    Hull, R., Narendra, N.C., Nigam, A.: Facilitating Workflow Interoperation Using Artifact-Centric Hubs. In: Baresi, L., Chi, C.-H., Suzuki, J. (eds.) ICSOC-ServiceWave 2009. LNCS, vol. 5900, pp. 1–18. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Walukiewicz, I.: Model Checking CTL Properties of Pushdown Systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 127–138. Springer, Heidelberg (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Francesco Belardinelli
    • 1
  • Alessio Lomuscio
    • 1
  • Fabio Patrizi
    • 1
  1. 1.Department of ComputingImperial College LondonUK

Personalised recommendations