SVeDaS: Specification and Verification of Data-aware Systems (ANR JCJC Project 16-CE40-0021-01)

Overview

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.

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, and to apply these results to the verification of auctions against strategic behaviours of agents, such as collusion and manipulation.

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 in e-markets;

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

  3. to analyse the formal properties of these 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 language fragments relevant for auction-driven applications, which have a decidable model checking problem and possibly are also amenable to practical verification;

  5. to develop the model checker SVeDaS for the verification and validation of data-aware systems in multi-agent scenarios;

  6. to evaluate the performance of the SVeDaS tool in popular auctioning mechanisms, including real-time bidding, and to release SVeDaS as open-source software.
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, including through the model checker SVeDaS. In turn, these contributions will help building more secure and reliable auction-based mechanisms for e-commerce and e- business.


List of publications

2019

2018 2017