CADP, qui signifie Construction and Analysis of Distributed Processes, est une suite logicielle qui aide les concepteurs de systèmes, les ingénieurs et les chercheurs à concevoir et à déboguer des systèmes distribués. Un système distribué se compose de plusieurs machines qui s’envoient des messages les unes aux autres. Les systèmes distribués sont notoirement difficiles à mettre en place car les temps de transmission ne sont pas fixés à l’avance, les machines peuvent tomber en panne, etc. et de nombreux cas doivent donc être pris en compte. Par exemple, il peut arriver qu’une machine attende qu’une autre machine ait terminé son travail, qui attend une autre machine, qui attend la première, et que le système soit bloqué (deadlock, ou interblocage).
Certains de ces cas peuvent être suffisamment rares ou compliqués pour ne pas être détectés lors des tests, mais ils peuvent se produire lorsque le système est déployé sur le terrain. CADP, en plus des tests, propose la vérification par le model-checking, c’est-à-dire l’exploration exhaustive de tous les cas qui peuvent se produire.
Les travaux sur CADP ont débuté à Verimag à la fin des années 1980, début des années 1990 (Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier…). Il s’agissait alors, afin de limiter l’explosion du coût du calcul de la vérification, de développer des approches compositionnelles (analyse séparée de composants du système) et de bisimulation (on regroupe les états possibles du système en classes d’états équivalents). Le développement de CADP a ensuite été transféré à l’INRIA Grenoble, où le groupe actuel sur CADP se compose d’Hubert Garavel, Frédéric Lang, Radu Mateescu et Wendelin Serwe.
À Verimag, la recherche se poursuit sur les approches qui aident à concevoir et à mettre en œuvre des systèmes informatiques sûrs et fiables, à la fois sur des aspects théoriques et plus appliqués. Verimag est une unité mixte de recherche du CNRS, de l’Université Grenoble Alpes et de Grenoble-INP.
Hubert Garavel, Frédéric Lang, and Laurent Mounier. Compositional Verification in Action. In Proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS’18), Maynooth University, Ireland, volume 11119 of Lecture Notes in Computer Science, pages 189-210. Springer, September 2018. http://cadp.inria.fr/publications/G...
Hubert Garavel and Frédéric Lang. Equivalence Checking 40 Years After : A Review of Bisimulation Tools. In A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, volume 13560 of Lecture Notes in Computer Science, pages 213-265. Springer, September 2022. https://link.springer.com/chapter/1...
