Automated Support for the Design and Validation of Parameterized Systems

The main and final goal of this project is to provide an automatic tool to support the design and validation of parameterized systems. This page is a collection of a series of single projects focusing on an extension of the infinite-state model-checker SAFARI, required either to gain a speed-up in solving certain tasks or for defining new solutions.

The increasing complexity of engineered systems makes verification processes a fundamental stage in software and hardware development. Nowadays, more and more distributed systems are applied in many heterogeneous field (sensors networks, e-commerce, distributed databases, real-time systems, mission-critical systems). One main feature distinguishes them from single-thread systems: their being parameterized in the number of the agents acting in their execution. Think about an operating system with many users, a database running on many servers, a protocol involving several processes: all these systems have to be verified keeping unknown the number of these agents. This feature makes classical formal verification technologies unsuitable for the verification of parameterized systems, because they requires to work with a system with a finite number of possible configurations, while the unknown number of agents makes the number of configurations unknown, hence potentially unbounded.
This problem is, in its general formulation, undecidable; however it has been shown that if the system under verification met certain hypotesis, a sound solution exists (solution that is also complete for a more restrictive class of hypotesis). This solution relies on the computational power of an infinite-state model-checker.

Goal(s) of the project

Required skills

Acquired competencies