Victor Vianu (Université San Diego Californie, et LSV, ENS Cachan)

Workflows centered around data are increasingly common. Recently, tools have been developed for high-level specification of such workflows and other data- driven applications. Such specification tools not only allow fast prototyping and improved programmer productivity but, as a side effect, provide convenient targets for automatic verification. A notable example is IBM’s business artifact framework, successfully deployed in practice.

In this talk I will present a formal model of data-centric workflows based on IBM’s business artifacts, and results on automatic verification of such processes. Artifacts are tuples of relevant values, equipped with local state relations and accessing an underlying database. They evolve under the action of services specified by pre-and-post conditions, that correspond to workflow tasks. The verification problem consists in statically checking whether all runs of an artifact system satisfy desirable properties, expressed in an extension of linear-time temporal logic. I will exhibit several classes of specifications and properties that can be automatically verified. The results are quite encouraging and suggest that, unlike arbitrary software systems, significant classes of data-centric workflows may be amenable to fully automatic verification. This relies on a novel marriage of techniques from the database and computer-aided verification areas.

The talk is based on joint work with Alin Deutsch, Elio Damaggio, Richard Hull and Fabio Patrizi.