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. © Springer-Verlag Berlin Heidelberg 2012.

Verification of GSM-based artifact-centric systems through finite abstraction / Francesco, Belardinelli; Alessio, Lomuscio; Patrizi, Fabio. - STAMPA. - 7636 LNCS:(2012), pp. 17-31. (Intervento presentato al convegno 10th International Conference on Service-Oriented Computing, ICSOC 2012 tenutosi a Shanghai; China) [10.1007/978-3-642-34321-6_2].

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

PATRIZI, FABIO
2012

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. © Springer-Verlag Berlin Heidelberg 2012.
2012
10th International Conference on Service-Oriented Computing, ICSOC 2012
industry; enterprise resource management; knowledge workers
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Verification of GSM-based artifact-centric systems through finite abstraction / Francesco, Belardinelli; Alessio, Lomuscio; Patrizi, Fabio. - STAMPA. - 7636 LNCS:(2012), pp. 17-31. (Intervento presentato al convegno 10th International Conference on Service-Oriented Computing, ICSOC 2012 tenutosi a Shanghai; China) [10.1007/978-3-642-34321-6_2].
File allegati a questo prodotto
File Dimensione Formato  
Belardinelli_Verification_2012.pdf

solo gestori archivio

Tipologia: Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 281.7 kB
Formato Adobe PDF
281.7 kB Adobe PDF   Contatta l'autore
VE_2012_11573-505090.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 330.59 kB
Formato Adobe PDF
330.59 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/505090
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 38
  • ???jsp.display-item.citation.isi??? ND
social impact