Introduction
The availability of wireless communications has tremendously increased in recent years. Such evolution brings new usages, and with them a wealth of practical and theoretical problems. It mandates to design new applications that make various communicating agents and terminals interact together, mostly autonomously.
This new paradigm of distributed system, called ubiquitous computing, leads to significant changes in telecommunications engineering that must be able to adapt to frequent changes in the communication graph, mainly due to the mobility of communicating agents. The dynamics of these distributed systems has a significant impact on the nature of the tasks that can be performed. Designing applications over such networks requires the ability to adapt to topology changes and to the lack of (static) logical structures such as trees, spanners, minimum dominating sets, the presence of a leader, etc.
The core of ESTATE consists in laying the foundations of a new algorithmic framework for enabling Autonomic Computing in distributed and highly dynamic systems and networks. In other words, we plan to design a model that includes the minimal algorithmic basis allowing the emergence of dynamic distributed systems with self-* capabilities, e.g., self-organization, self-healing, self-configuration, self-management, self-optimization, self-adaptiveness, or self-repair.
Objectives
In order to do this, we consider three main research workpackages:
- Workpackage #1 consists of building the theoretical foundations of autonomic computing in dynamic systems. We consider self-stabilization as a practical approach to implement distributed basic algorithms enabling Autonomic Computing.
- Workpackage #2 aims at enhancing the safety in some cases. We plan to revisit specializations of self-stabilization in the context of dynamic environments. We aim at establishing the minimum requirements in terms of amount or type of dynamics to allow some strong safety guarantees.
- Workpackage #3 aims at providing additional formal guarantees by proposing a general framework based on the Coq proof assistant to (semi-)automatically construct certified proofs for both Workpackage #1 and #2. To that end, we will identify adequate formal models and general proof schemes used to show the correctness of algorithms.
These workpackages will interact with each other as follows. The first one brings lower bounds and limitations to the second, which in turn provides use cases and problems to the former. The third action aims at providing certified proofs of theoretical results obtained in both the first and second actions, e.g., impossibility results, complexity bounds, and correctness of distributed algorithms. Algorithms provided by Workpackage #1 and Workpackage #2 will be validated through four complementary approaches: (i) classical "by-hand" proofs, (ii) (semi-)automatically certified proofs given by Workpackage #3, (iii) by simulations, and (iv) in real mobility context. Approches (iii) and (iv) will be implemented on dedicated platforms.
Partners
VERIMAG People involved
- Karine Altisen
- Pierre Corbineau
- Stéphane Devismes
- Anaïs Durand
