An artifact-centric service is a stateful service that holistically represents both the data and the process in terms of a (dynamic) artifact. An artifact is constituted by a data component, holding all the data of interest for the service, and a lifecycle, which specifies the process that the service enacts. In this paper, we study artifact-centric services whose data component is a full-fledged relational database, queried through (first-order) conjunctive queries, and the lifecycle component is specified as sets of condition-action rules, where actions are tasks invocations, again based on conjunctive queries. Notably, the database can evolve in an unbounded way due to new values (unknown at verification time) inserted by tasks. The main result of the paper is that verification in this setting is decidable under a reasonable restriction on the form of tasks, called weak acyclicity, which we borrow from the recent literature on data exchange. In particular, we develop a sound, complete and terminating verification procedure for sophisticated temporal properties expressed in a first-order variant of μ-calculus. © 2012 World Scientific Publishing Company.
Verification of conjunctive artifact-centric services / DE GIACOMO, Giuseppe; DE MASELLIS, Riccardo; Rosati, Riccardo. - In: INTERNATIONAL JOURNAL OF COOPERATIVE INFORMATION SYSTEMS. - ISSN 0218-8430. - 21:2(2012), pp. 111-139. [10.1142/S0218843012500025]
Verification of conjunctive artifact-centric services
DE GIACOMO, Giuseppe;DE MASELLIS, RICCARDO;ROSATI, Riccardo
2012
Abstract
An artifact-centric service is a stateful service that holistically represents both the data and the process in terms of a (dynamic) artifact. An artifact is constituted by a data component, holding all the data of interest for the service, and a lifecycle, which specifies the process that the service enacts. In this paper, we study artifact-centric services whose data component is a full-fledged relational database, queried through (first-order) conjunctive queries, and the lifecycle component is specified as sets of condition-action rules, where actions are tasks invocations, again based on conjunctive queries. Notably, the database can evolve in an unbounded way due to new values (unknown at verification time) inserted by tasks. The main result of the paper is that verification in this setting is decidable under a reasonable restriction on the form of tasks, called weak acyclicity, which we borrow from the recent literature on data exchange. In particular, we develop a sound, complete and terminating verification procedure for sophisticated temporal properties expressed in a first-order variant of μ-calculus. © 2012 World Scientific Publishing Company.File | Dimensione | Formato | |
---|---|---|---|
VE_2012_11573-484867.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
408.63 kB
Formato
Adobe PDF
|
408.63 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.