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.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.