AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Kaiserslautern

In this talk I present our recent results on data-aware static verification, in which we select the artifact-centric model as a natural vehicle for our investigation. Artifact-centric systems are models for business process systems in which the dynamics and the manipulation of data are equally central. Given the family of variations on this model found in the literature, for the sake of a uniform terminology we introduce our own pristine formalization, which captures existing artifact-centric dialects, and which is semantically equivalent to the most expressive ones. We call our business process formalism ``Data-Centric Dynamic Systems'' (DCDS). The process is described in terms of atomic actions that evolve the system. Action execution may involve calls to external services, thus inserting fresh data into the system. As a result such systems are infinite-state. We show that verification is undecidable in general, and we isolate notable cases where decidability is achieved. More specifically, we show that in a first-order $\mu$-calculus variant that preserves knowledge of objects appeared along a run, we get decidability under the assumption that the fresh data introduced along a run are bounded, though they might not be bounded in the overall system. Then, we investigate decidability under the assumption that knowledge of objects is preserved only if they are continuously present. We show that if infinitely many values occur in a run but do not accumulate in the same state, then we get again decidability. We give syntactic conditions to avoid this accumulation through the novel notion of ``generate-recall acyclicity'', which ensures that every service call activation generates new values that cannot be accumulated indefinitely. We believe that DCDSs are natural and expressive models for systems powered by an underlying database (i.e., so called data-centric systems), and thus are an ideal vehicle for foundational research with potential to transfer to alternative models.

Susanne Rock

0631-9303-9605

--email hidden

Yes

Saarbrücken

E1 5

029

passcode not visible

logged in users only