Abstract
Artifact systems are a novel paradigm for implementing service oriented computing. Business artifacts include both data and process descriptions at interface level thereby providing more sophisticated and powerful service inter-operation capabilities. In this paper we put forward a technique for the practical verification of business artifacts in the context of multi-agent systems. We extend GSM, a modelling language for artifact systems, to multi-agent systems and map it into a variant of AC-MAS, a semantics for reasoning about artifact systems. We introduce a symbolic model checker for verifying GSM-based multi-agent systems. We evaluate the tool on a scenario from the service community.
This research was supported by the EU FP7 projects ACSI (FP7-ICT-257593). Work by the author Andreas Griesmayer was conducted in part at Imperial College London and supported by the Marie Curie Fellowship “DiVerMAS” (FP7-PEOPLE-252184). Alessio Lomuscio acknowledges support from the UK EPSRC through the Leadership Fellowship grant “Trusted Autonomous Systems” (EP/I00520X/1).
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
Singh, M., Rao, A.S., Georgeff, M.: Formal methods in DAI: Logic-based representation and reasoning. In: Weiß, G. (ed.) Multiagent Systems: A Modern Approach to Distributed Artifical Intelligence, pp. 331–376. MIT Press (1999)
Bultan, T., Su, J., Fu, X.: Analyzing conversations of web services. IEEE Internet Computing 10(1), 18–25 (2006)
Lomuscio, A., Qu, H., Solanki, M.: Towards verifying contract regulated service composition. Autonomous Agents and Multi-Agent Systems 24(3), 345–373 (2012)
Singh, M.P., Huhns, M.N.: Service-oriented computing - semantics, processes, agents. Wiley (2005)
Baldoni, M., Baroglio, C., Mascardi, V.: Special issue: Agents, web services and ontologies: Integrated methodologies. Multiagent and Grid Systems 6(2), 103–104 (2010)
Cohn, D., Hull, R.: Business artifacts: A data-centric approach to modeling business operations and processes. Bulletin of the IEEE Computer Society Technical Committee on Data Engineering 32(3), 3–9 (2009)
Hull, R., Damaggio, E., De Masellis, R., et al.: Business artifacts with guard-stage-milestone lifecycles: managing artifact interactions with conditions and events. In: Proceedings of the International Conference on Distributed Event-Based Systems (DEBS 2011), pp. 51–62 (2011)
Object Management Group: Proposal for: Case management modeling and notation (CMMN) specification 1.0, Document bmi/12-02-09 (February 2012)
Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. Journal of Computer and System Sciences 73(3), 442–474 (2007)
Hariri, B.B., Calvanese, D., Giacomo, G.D., Deutsch, A., Montali, M.: Verification of relational data-centric dynamic systems with external services. CoRR (2012)
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)
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)
Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verifying GSM-based business artifacts. In: Proceedings of ICWS 2012, pp. 25–32 (2012)
Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proceedings of Principles of Knowledge Representation and Reasoning (KR 2012), pp. 319–328 (2012)
Parikh, R., Ramanujam, R.: Distributed processes and the logic of knowledge. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 256–268. Springer, Heidelberg (1985)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. The MIT Press (1995)
Somenzi, F.: CUDD: CU decision diagram package - release 2.5.0 (2012), http://vlsi.colorado.edu/~fabio/CUDD/ (January 2013)
Lomuscio, A., Qu, H., Raimondi, F.: Mcmas: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)
Shoham, S., Grumberg, O.: 3-valued abstraction: More precision at less cost. Information and Computation 206(11), 1313–1333 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Gonzalez, P., Griesmayer, A., Lomuscio, A. (2014). Model Checking GSM-Based Multi-Agent Systems. In: Lomuscio, A.R., Nepal, S., Patrizi, F., Benatallah, B., Brandić, I. (eds) Service-Oriented Computing – ICSOC 2013 Workshops. ICSOC 2013. Lecture Notes in Computer Science, vol 8377. Springer, Cham. https://doi.org/10.1007/978-3-319-06859-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-06859-6_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06858-9
Online ISBN: 978-3-319-06859-6
eBook Packages: Computer ScienceComputer Science (R0)