FoRmal mEthods for the Design of Distributed Algorithms – FREDDA

Distributed algorithms are nowadays omnipresent in most systems and applications. It is of utmost importance to develop algorithmic solutions that are both robust and flexible, to be used in large scale applications. In the last decades, researchers from the distributed computing community have
developed advanced techniques for the design and analysis of
distributed algorithms. One of the key aspects in the development of
these algorithms are the specific assumptions made on the considered
execution context. For example, communication can be synchronous or asynchronous, the entities in the network may or may not be equipped with a unique identifier, or a certain number of errors and failures can happen during an execution. These assumptions are crucial and may lead to different families of algorithms designed for a specific context. While there are numerous sophisticated techniques for algorithm design and analysis, most of the existing distributed algorithms remain tailored to one
very specific system model and are
surprisingly difficult to generalize to different, but very
similar models.
Furthermore, correctness proofs of distributed algorithms are extremely intricate.
On top of this comes the fact that most algorithms are designed for an unspecified, unbounded number of participants and may use resources (like registers or data transmitted in messages) that depend on that number. Moreover, their correctness proofs strongly depend on the underlying execution context and, as a matter of fact,
can be very sensitive to any deviation. In other words, distributed algorithms tend to be not robust.

The purpose of our project is to develop formal methods that provide algorithmic support for the design of robust distributed algorithms. The robustness of distributed algorithms is a challenging problem that has not been much considered until now, and there is no systematic way to guarantee or verify the behavior of an algorithm beyond the context for which it has been designed. We propose to develop automated formal method techniques to verify the robustness of distributed algorithms and to support the development of robust applications. Our methods are of two kinds: statically through classical verification, and dynamically, by synthesizing distributed monitors, that check either correctness or the validity of the context hypotheses at runtime.

The methods and tools we will provide to perform robustness analysis will be integrated in a development cycle whose role will be to build robust algorithms starting from an algorithm which is correct in a certain context. This cycle will work as follows: it firsts test whether the input algorithm is correct in the new execution context, in case of a positive answer, it outputs the algorithm, in case of a negative answer, our analysis produces a counter-example for the robustness which can be used by experts in distributed computing to modify the algorithm in order to discard the non-robust behavior. After a certain number of iterations of such a cycle an algorithm which is more robust than the one originally considered is obtained.

To develop methods for the robustness analysis of distributed algorithms we have grouped researchers from both distributed computing community and formal methods community. We have hence experts in two areas with complementary skills. On one side, we have the distributed computing community with its know-how for establishing the correctness of a few particular distributed algorithms using ad-hoc techniques that strongly depend on the execution context. On the other side, the verification community provides formal models and automated analysis techniques.