Prix de l’épreuve du temps pour la boîte à outils CADP

Les travaux sur la boîte à outils CADP ont commencé au laboratoire Verimag à la fin des années 1980, début des années 1990, avec le concours de Jean-Claude Fernandez, anciennement professeur à l'Université Grenoble Alpes et membre du laboratoire Verimag, Hubert Garavel, actuellement directeur de recherche INRIA au Laboratoire d’Informatique de Grenoble (LIG - CNRS/Université Grenoble Alpes) et Laurent Mounier, actuellement maître de conférences à l’Université Grenoble Alpes et membre du laboratoire Verimag.

À cette période, il s’agissait 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), afin de limiter l’explosion du coût du calcul de la vérification.

C’est pour répondre à cet objectif que le projet CADP, qui signifie Construction and Analysis of Distributed Processes, a été initié. Cette boîte à outils 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. Ceux-ci sont notoirement difficiles à mettre en place, car les temps de transmission ne sont pas fixés à l'avance, les machines peuvent tomber en panne, 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 elle-même 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. La boîte à outils CADP, en plus des tests, propose la vérification par model-checking, c'est-à-dire l'exploration exhaustive de tous les cas qui peuvent se produire.

Ces travaux ont été récompensés par le Test-of-Time Award de la conférence ETAPS, conférence européenne de référence dans le domaine de la vérification logicielle.

Le développement de la boîte à outils a par la suite été transféré au Centre Inria de Grenoble. Le groupe de travail se compose d'Hubert Garavel et Frédéric Lang, chargés de recherche Inria au LIG, Radu Mateescu, directeur de recherche Inria au LIG et Wendelin Serwe, chargé de recherche Inria au LIG.

Quant au laboratoire Verimag, il poursuit ses recherches 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.