A first category of work focuses on fault tolerance in distributed systems, in the presence of failing nodes or broken links. The problem arises at different scales, from large-scale communication infrastructures to multi- or manycore hardware architectures. Graphs provide a convenient abstraction of the connection structure. At large scale, we study rerouting strategies to ensure message delivery while minimizing the impact on traffic congestion and path length [1,2]. The guarantees that can be provided depend on the structural properties of the underlying graphs. At a smaller scale, the challenge is to implement synchronization mechanisms between nodes to solve fundamental fault tolerance problems such as consensus [3]. Again, a structural perspective is relevant and raises many computability issues [4].

The second category of work, on algorithms for automated verification, relies on behavioral models to express parallelism, communication, temporal constraints, and, more recently, hybrid systems. The challenge is to improve the scalability of model checking tools. This requires novel abstraction and optimization techniques for symbolic state representation [5]. An important aspect of our work is the implementation of model checking algorithms in mature tools, in which we invest a long-term development effort. Two key examples are TINA, a toolbox for the analysis of temporal Petri nets that has won several awards at TOOLympics competitions, and Fiacre, a specification language for expressing the behavior of reactive and real-time systems.

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.