PARameterized DIstributed Systems Verification – PARDI

The overall objective of PARDI is the formal, machine-supported verification of parameterized distributed systems. A parameterized system specification is a specification for a whole class of systems, parameterized by the number of entities and the properties of the interaction, such as the communication model (synchronous/asynchronous, order of delivery of message, application ordering) or the fault model (crash failure, message loss). To be able to verify such systems without explicitly instantiating all the parameters, new theoretical results and dedicated tools are required. Due to the fundamental undecidability of the problem, automatic tools are not powerful enough to verify rich parameterized systems: they are limited in their expressiveness and do not handle the variety of the interaction models. To assist and automate verification without parameter instantiation, PARDI uses two complementary approaches. First, a fully automatic model checker modulo theories is considered. Then, to go beyond the intrinsic limits of parameterized model checking, the project advocates a collaborative approach between proof assistant and model checker. This collaboration is two-ways: in one direction, the model checker is used as an explorer to generate elementary invariants that can be used and combined in interactive verification; in the other direction, a property which is needed by the proof assistant is discharged to the parameterized model checker.

Cubicle, a model checker for array-based systems, and TLAPS, a proof assistant well-adapted to study distributed algorithms, are the basis of this project. Using case studies, both in parameterized distributed systems and in parameterized workflow-based systems, a theoretical analysis is required to exhibit the relevant parameters and to prove generic results (e.g. substitutability). This analysis is needed to define the richer data structures that will extend the model checker's expressiveness, and to inject these generic results into checkers and provers.

A first contribution of the project will be the verification of parameterized distributed systems, for an arbitrary number of sites. A library of results for the many communication models and fault models which exist and their integration in the verification tools will be a second contribution. A third contribution will be the design and implementation of a verification toolchain based on a close interaction between a proof assistant and a model checker. A fourth contribution will be a new DSL for parameterized workflow-based systems with rich explicit parameterization features, and its translation into the checker and prover input language.