Verification of Data-aware Systems: Abstraction Techniques and Decidability Results

14^th February 2012, 15:00 Ashton Lecture Theatre
Dr. Francesco Belardinelli
Department of Computing
Imperial College London
UK

Abstract

Data-aware systems (DaS) are a novel paradigm in web-services. Differently from the standard process-based approach, in DaS data are given the same prominence as processes. The implementations of DaS involve the composition of several databases on which services operate. This emphasis on data leads to an infinite state-space for the model checking problem. A possibly infinite data domain also call for specification languages that support quantification, e.g., first-order multi-modal logics. This setting is known to generate an undecidable model checking problem, thereby reducing, at least theoretically, the
possibility of DaS verification.

In this talk I will present abstraction techniques that can be deployed to make the model checking problem amenable, thus obtaining decidability results for some specific classes of DaS. These results enable the verification of basic temporal-epistemic properties of DaS when analysed under a number of conditions.

The research presented in this talk has received funding within the EU STREP Project ACSI.