## Seminar in CS&E -- Fabio Patrizi -- Friday June 24, 2011

When: Friday June 24, 2011 12:00

Where: Aula Magna DIS, Via Ariosto 25, 00185, Roma

Speaker: Fabio Patrizi, Department of Computing, Imperial College London, UK

Title: Verification of Deployed Artifact Systems via Data Abstraction

Abstract

Artifact systems are a novel paradigm for specifying and

implementing business processes described in terms of interacting

modules called artifacts. Artifacts consist of data and lifecycle

models, accounting for the relational structure of the artifact

state and its possible evolutions over time.

We consider the problem of verifying artifact systems against

specifications expressed in a first-order extension of branching-time

temporal logic. This problem is undecidable in general, as, put simply,

each state is a database instance with elements coming from an infinite

domain, and there is no regularity one can exploit to decide whether the

system satisfies an arbitrary property.

The work focuses on a decidable (bounded) variant of the problem, where

the states of the system can only accommodate a bounded number of

distinct elements. Even under this assumption the system contains an

infinite number of states. However, a data abstraction technique can be

used to reduce the problem to standard model checking.

Interestingly, in some cases solving the bounded version of a generic

instance is informative with respect to the original instance, too.

In this talk, I will introduce the problem, give an overview of the

abstraction technique, describe the relationship between the bounded and

the general formulations, and discuss possible future directions.

CS&E WWW page: http://www.dis.uniroma1.it/~seminf/