Specification and Verification of Data-aware Systems – SVeDaS

In recent years data-aware systems have been proposed as a comprehensive framework to model complex business workflows by considering data and processes as equally relevant tenets of the system description [19, 28]. This setting is particularly suited to model auctions and auction-based mechanisms in electronic commerce [20].

The SVeDaS project is designed to advance the state-of-the-art in the modelling, analysis and deployment of data-aware systems by using a novel, compositional, agent-based approach to their specification and verification.

The main objectives of the SVeDaS project can be summarized as follows:

1. to introduce agent-based, computationally-grounded models for data-aware systems, that are capable of expressing rich business workflows, including auction-based mechanisms and e-markets;

2. to explore logic-based formal languages for the specification of strategic behaviours of autonomous agents (including robustness
against malicious behaviours, as well as manipulability and collusion in auctions) pertaining to business processes and agents operating on them;

3. to analyse the formal properties of the data-aware models, particularly the issues concerning formal verification by model checking in contexts of imperfect information;

4. to find classes of data-aware systems and expressive logical fragments that have a decidable model checking problem, and possibly are also amenable to practical verification;

5. to develop model checking tools and techniques for the verification and validation of data-aware systems in multi-agent scenarios, with a focus on auctioning mechanisms.

We anticipate that the results of the SVeDaS project will contribute significantly to our understanding of data-aware systems, thus improving the design and management of business processes by formal verification through model checking. In turn, these contributions will help building more secure and reliable systems, as well as reducing the costs of faults in auction-based mechanisms for e-commerce and e-business.