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

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: