Article

Verification of GSM-Based artifact-centric systems through finite abstraction

Authors:

Francesco Belardinelli,

Alessio Lomuscio,

Fabio PatriziAuthors Info & Claims

ICSOC'12: Proceedings of the 10th international conference on Service-Oriented Computing

Pages 17 - 31

https://doi.org/10.1007/978-3-642-34321-6_2

Published: 12 November 2012 Publication History

Abstract

The GSM framework provides a methodology for the development of artifact-centric systems, an increasingly popular paradigm in service-oriented computing. In this paper we tackle the problem of verifying GSM programs in a multi-agent system setting. We provide an embedding from GSM into a suitable multi-agent systems semantics for reasoning about knowledge and time at the first-order level. While we observe that GSM programs generate infinite models, we isolate a large class of "amenable" systems, which we show admit finite abstractions and are therefore verifiable through model checking. We illustrate the contribution with a procurement use-case taken from the relevant business process literature.

References

[1]

Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995)

[2]

Belardinelli, F., Lomuscio, A., Patrizi, F.: A computationally-grounded semantics for artifact-centric systems and abstraction results. In: Proc. of IJCAI (2011)

[3]

Belardinelli, F., Lomuscio, A., Patrizi, F.: Verification of Deployed Artifact Systems via Data Abstraction. In: Kappel, G., Maamar, Z., Motahari-Nezhad, H. R. (eds.) ICSOC 2011. LNCS, vol. 7084, pp. 142-156. Springer, Heidelberg (2011)

[4]

Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proc. of KR (2012)

[5]

Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.: View-based query answering in description logics: Semantics and complexity. J. Comput. Syst. Sci. 78(1), 26-46 (2012)

[6]

Cohen, M., Dam, M., Lomuscio, A., Russo, F.: Abstraction in model checking multi-agent systems. In: Proc. of AAMAS (2) (2009)

[7]

Cohen, M., Dam, M., Lomuscio, A., Qu, H.: A Data Symmetry Reduction Technique for Temporal-epistemic Logic. In: Liu, Z., Ravn, A. P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 69-83. Springer, Heidelberg (2009)

[8]

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)

[9]

Damaggio, E., Hull, R., Vaculín, R.: On the Equivalence of Incremental and Fixpoint Semantics for Business Artifacts with Guard-Stage-Milestone Lifecycles. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM2011. LNCS, vol. 6896, pp. 396-412. Springer, Heidelberg (2011)

[10]

Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proc. of ICDT (2009)

[11]

Deutsch, A., Sui, L., Vianu, V.: Specification and Verification of Data-Driven Web Applications. J. Comput. Syst. Sci. 73(3), 442-474 (2007)

[12]

Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. The MIT Press (1995)

[13]

Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verifying GSM-based business artifacts. In: Proc. of ICWS (2012)

[14]

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)

[15]

Hull, R., Damaggio, E., De Masellis, R., Fournier, F., Gupta, M., Heath, F. T., Hobson, S., Linehan, M. H., Maradugu, S., Nigam, A., Sukaviriya, P. N., Vaculín, R.: Business artifacts with guard-stage-milestone lifecycles: managing artifact interactions with conditions and events. In: Proc. of DEBS (2011)

[16]

Lomuscio, A., Penczek, W., Qu, H.: Partial Order Reductions for Model Checking Temporalepistemic Logics over Interleaved Multi-agent Systems. Fundamenta Informaticae 101(1-2), 71-90 (2010)

[17]

Lomuscio, A., Qu, H., Solanki, M.: Towards verifying contract regulated service composition. Journal of Autonomous Agents and Multi-Agent Systems 24(3), 345-373 (2012)

Cited By

Deutsch ALi YVianu V(2019)Verification of Hierarchical Artifact SystemsACM Transactions on Database Systems10.1145/332148744:3(1-68)Online publication date: 5-Jun-2019
https://dl.acm.org/doi/10.1145/3321487
Amiri MAgrawal DHung CPapadopoulos G(2019)VIEWProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297291(85-93)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297291
Abdulla PAiswarya CAtig MMontali MSuciu DSkritek SKoch C(2019)Reachability in Database-driven Systems with Numerical Attributes under Recency BoundingProceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3294052.3319705(335-352)Online publication date: 25-Jun-2019
https://dl.acm.org/doi/10.1145/3294052.3319705
Show More Cited By

Verification of GSM-Based artifact-centric systems through finite abstraction
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation

Recommendations

Verification of GSM-Based Artifact-Centric Systems by Predicate Abstraction
Service-Oriented Computing
Abstract
Artifact-centric systems are a recent paradigm to model and implement business workflows. They describe data, processes, internal and external agents and include mechanisms for data hiding and access control. GSM is a language for the ...
Abstraction-based deductive-algorithmic verification of reactive systems
Abstraction-based Deductive-Algorithmic Verification of Reactive Systems

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ICSOC'12: Proceedings of the 10th international conference on Service-Oriented Computing

November 2012

789 pages

ISBN:9783642343209

Editors:
Chengfei Liu
Faculty of ICT, Swinburne University of Technology, John Street, Hawthorn, VIC, Australia
,
Heiko Ludwig
Faculty of ICT, IBM Almaden Research Center, 650 Harry Road, San Jose, CA, Australia
,
Farouk Toumani
LIMOS - UMR 6158, Blaise Pascal University, Complexe scientifique des Cézeaux, Aubiere, CA, France
,
Qi Yu
College of Computing and Information Sciences, Rochester Institute of Technology, 1 Lomb Memorial Drive, Rochester, NY, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 12 November 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Deutsch ALi YVianu V(2019)Verification of Hierarchical Artifact SystemsACM Transactions on Database Systems10.1145/332148744:3(1-68)Online publication date: 5-Jun-2019
https://dl.acm.org/doi/10.1145/3321487
Amiri MAgrawal DHung CPapadopoulos G(2019)VIEWProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297291(85-93)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297291
Abdulla PAiswarya CAtig MMontali MSuciu DSkritek SKoch C(2019)Reachability in Database-driven Systems with Numerical Attributes under Recency BoundingProceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3294052.3319705(335-352)Online publication date: 25-Jun-2019
https://dl.acm.org/doi/10.1145/3294052.3319705
Eshuis RHull RYi M(2019)Reasoning About Property Preservation in Adaptive Case ManagementACM Transactions on Internet Technology10.1145/317777819:1(1-21)Online publication date: 25-Jan-2019
https://dl.acm.org/doi/10.1145/3177778
Steinau SMarrella AAndrews KLeotta FMecella MReichert M(2019)DALECSoftware and Systems Modeling (SoSyM)10.1007/s10270-018-0695-018:4(2679-2716)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10270-018-0695-0
Belardinelli FMalvone V(2019)Decidable Verification of Agent-Based Data-Aware SystemsPRIMA 2019: Principles and Practice of Multi-Agent Systems10.1007/978-3-030-33792-6_4(52-68)Online publication date: 28-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-33792-6_4
Deutsch AHull RLi YVianu V(2018)Automatic verification of database-centric systemsACM SIGLOG News10.1145/3212019.32120255:2(37-56)Online publication date: 30-Apr-2018
https://dl.acm.org/doi/10.1145/3212019.3212025
Steinau SAndrews KReichert M(2018)Modeling Process Interactions with Coordination ProcessesOn the Move to Meaningful Internet Systems. OTM 2018 Conferences10.1007/978-3-030-02610-3_2(21-39)Online publication date: 22-Oct-2018
https://dl.acm.org/doi/10.1007/978-3-030-02610-3_2
Li YDeutsch AVianu V(2017)VERIFASProceedings of the VLDB Endowment10.14778/3157794.315779811:3(283-296)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.14778/3157794.3157798
Hull R(2017)BlockchainProceedings of the 11th ACM International Conference on Distributed and Event-based Systems10.1145/3093742.3097982(2-4)Online publication date: 8-Jun-2017
https://dl.acm.org/doi/10.1145/3093742.3097982
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents