Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
Belardinelli, F., Lomuscio, A., Patrizi, F.: A Computationally-Grounded Semantics for Artifact-Centric Systems and Abstraction Results. In: Proc. of IJCAI (to appear, 2011)
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)
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)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers 58, 118–149 (2003)
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)
Caucal, D.: On Infinite Transition Graphs having a Decidable Monadic Theory. Theoretical Computer Science 290(1), 79–115 (2003)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (2000)
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)
Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic Verification of Data-centric Business Processes. In: Proc. of ICDT (2009)
Deutsch, A., Sui, L., Vianu, V.: Specification and Verification of Data-Driven Web Applications. J. Comput. Syst. Sci. 73(3), 442–474 (2007)
Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic, vol. 148. Elsevier (2003)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Belardinelli, F., Lomuscio, A., Patrizi, F. (2011). Verification of Deployed Artifact Systems via Data Abstraction. In: Kappel, G., Maamar, Z., Motahari-Nezhad, H.R. (eds) Service-Oriented Computing. ICSOC 2011. Lecture Notes in Computer Science, vol 7084. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25535-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-25535-9_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25534-2
Online ISBN: 978-3-642-25535-9
eBook Packages: Computer ScienceComputer Science (R0)