Programmation, Vérification, et Synthèse de Systèmes Distribués Adéquatement Consistent – AdeCoDS

Développer des systèmes distribués corrects, performants et disponibles est un défi majeur. En pratique, la cohérence forte doit souvent être sacrifiée, ce qui rend la tâche des programmeurs extrêmement difficile. Un problème central est de déterminer un niveau de cohérence adéquat pour une application donnée: niveau qui nécessite le moins de synchronisation possible, mais qui est suffisamment fort pour assurer un fonctionnement correct de l’application. Le but de ce projet est de fournir une approche automatisée pour la co-conception d’une application avec son modèle de cohérence adéquat. Notre approche englobe des techniques de langages de programmation, de vérification formelle, et de conception de protocoles distribués. Ce projet propose de développer des méthodes de vérification et de synthèse de programmes s’exécutant sur des modèles de cohérence faible, exploiter ces méthodes pour fournir un cadre pour la conception et le développement de programmes à la fois corrects et efficaces (ayant de bonnes propriétés de disponibilité et de performance), et démontrer l’applicabilité de ce cadre en pratique (une application pour la gestion du réseau 5G+ et une application IoT).