Algorithmes et méthodes formelles
Les travaux figurant dans ce thème ont pour point commun de s’intéresser à des problèmes fondamentaux, résolus par la recherche d’algorithmes offrant des garanties formelles. Ils peuvent être classés en deux grandes catégories : algorithmique pour la tolérance aux fautes, et algorithmique pour la vérification automatique.
Une première grande catégorie de travaux s’intéresse à la tolérance aux fautes dans les systèmes répartis en présence de noeuds défaillants ou de liens cassés. Le problème se décline à de multiples échelles, de la grande infrastructure de communication à l’architecture matérielle multi- ou manycore. Les contributions algorithmiques s’appuient sur une abstraction de la structure de connexion sous forme de graphe. A grande échelle, nous étudions des stratégies de re-routage, pour assurer la délivrance des messages tout en minimisant l’impact sur la congestion du trafic et la longueur des chemins d’acheminement [1,2]. Les garanties possibles dépendent des propriétés structurelles des graphes sous-jacents. À plus petite échelle, l’enjeu est de mettre en œuvre des mécanismes de synchronisation entre les nœuds, pour résoudre des problèmes fondamentaux en tolérance aux fautes comme le consensus [3]. Là encore, une perspective structurelle est pertinente et ouvre de nombreuses questions de calculabilité [4].
La deuxième grande catégorie de travaux, relative à l’algorithmique pour la vérification automatique, s’appuie sur des modèles comportementaux permettant d’exprimer le parallélisme, la communication, les contraintes temporelles et, depuis peu, les systèmes hybrides. L’enjeu est de permettre le passage à l’échelle des outils de model checking. Ceci passe par des abstractions et des techniques d’optimisation de représentation symbolique d’états [5]. Un point fort de ces travaux concerne la valorisation des algorithmes de model checking au sein d’outils matures, dont le développement représente un effort de longue haleine. Deux exemples phares sont TINA, une boîte à outils pour l’analyse des réseaux de Petri temporels plusieurs fois primé aux compétitions TOOLympics, et Fiacre, un langage de spécification permettant d’exprimer le comportement des systèmes réactifs et temps-réel.
Références
[1] Klaus-Tycho Foerster, Juho Hirvonen, Yvonne-Anne Pignolet, Stefan Schmid, Gilles Trédan, "On the Price of Locality in Static Fast Rerouting", Proc. 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2022), pp. 215-226, 2022.
[2] Klaus-Tycho Foerster, Andrzej Kamisinski, Yvonne-Anne Pignolet, Stefan Schmid, Gilles Trédan, "Improved Fast Rerouting Using Postprocessing", IEEE Transactions on Dependable and Secure Computing, vol. 19, no. 1, pp. 537-550, 2022.
[3] Armando Castañeda, Pierre Fraigniaud, Ami Paz, Sergio Rajsbaum, Matthieu Roy, Corentin Travers, "Synchronous t-resilient consensus in arbitrary graphs", Information and Computation, vol. 292, 2023.
[4] Armando Castañeda, Pierre Fraigniaud, Ami Paz, Sergio Rajsbaum, Matthieu Roy, Corentin Travers, “A topological perspective on distributed network algorithms", Theoretical Computer Science, vol. 849, pp. 121-137, 2021.
[5] Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan, "Leveraging polyhedral reductions for solving Petri net reachability problems", International Journal on Software Tools for Technology Transfer, vol. 25, no. 1, pp. 95-114, 2023.