Artifacts are entities characterized by data of interest (constituting the state of the artifact) in a given business application, and a lifecycle, which constrains the artifact's possible evolutions. In this paper we study relational artifacts, where data are represented by a full fledged relational database, and the lifecycle is described by a temporal/dynamic formula expressed in μ-calculus. We then consider business processes, modeled as a set of condition/action rules, in which the execution of actions (aka tasks, or atomic services) results in new artifact states. We study conformance of such processes wrt the artifact lifecycle as well as verification of temporal/dynamic properties expressed in μ-calculus. Notice that such systems are infinite-state in general, hence undecidable. However, inspired by recent literature on database dependencies developed for data exchange, we present a natural restriction that makes such systems finite-state, and the above problems decidable. © 2011 Springer-Verlag.

Foundations of relational artifacts verification / Babak Bagheri, Hariri; Diego, Calvanese; DE GIACOMO, Giuseppe; DE MASELLIS, Riccardo; Felli, Paolo. - 6896 LNCS:(2011), pp. 379-395. (Intervento presentato al convegno 9th International Conference on Business Process Management, BPM 2011 tenutosi a Clermont-Ferrand nel 30 August 2011 through 2 September 2011) [10.1007/978-3-642-23059-2_28].

Foundations of relational artifacts verification

DE GIACOMO, Giuseppe;DE MASELLIS, RICCARDO;FELLI, PAOLO
2011

Abstract

Artifacts are entities characterized by data of interest (constituting the state of the artifact) in a given business application, and a lifecycle, which constrains the artifact's possible evolutions. In this paper we study relational artifacts, where data are represented by a full fledged relational database, and the lifecycle is described by a temporal/dynamic formula expressed in μ-calculus. We then consider business processes, modeled as a set of condition/action rules, in which the execution of actions (aka tasks, or atomic services) results in new artifact states. We study conformance of such processes wrt the artifact lifecycle as well as verification of temporal/dynamic properties expressed in μ-calculus. Notice that such systems are infinite-state in general, hence undecidable. However, inspired by recent literature on database dependencies developed for data exchange, we present a natural restriction that makes such systems finite-state, and the above problems decidable. © 2011 Springer-Verlag.
2011
9th International Conference on Business Process Management, BPM 2011
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Foundations of relational artifacts verification / Babak Bagheri, Hariri; Diego, Calvanese; DE GIACOMO, Giuseppe; DE MASELLIS, Riccardo; Felli, Paolo. - 6896 LNCS:(2011), pp. 379-395. (Intervento presentato al convegno 9th International Conference on Business Process Management, BPM 2011 tenutosi a Clermont-Ferrand nel 30 August 2011 through 2 September 2011) [10.1007/978-3-642-23059-2_28].
File allegati a questo prodotto
File Dimensione Formato  
VE_2011_11573-408676.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 434.68 kB
Formato Adobe PDF
434.68 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/408676
 Attenzione

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

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