CADP, which stands for Construction and Analysis of Distributed Processes, is a software suite that helps system designers, engineers and researchers design and debug distributed systems. A distributed system consists of several machines that send messages to each other. Distributed systems are notoriously difficult to get right because transmission times are not fixed in advance, machines may fail etc. and thus many cases have to be considered. For instance, it may happen that in some case, a machine waits for another machine to finish its work, which waits for another one, which waits for the first one, and the system is deadlocked.
Some of these cases may be sufficiently rare or convoluted that they are not detected when testing, but they might occur when the system is deployed in the field. CADP, in addition to testing, supports verification through model-checking, that is, exhaustive exploration of all cases that may occur.
Work on CADP began at Verimag in the late 1980s and early 1990s (Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier…). In order to limit the explosion of the computational cost of verification, the aim was to develop compositional approaches (separate analysis of system components) and bisimulation (the possible states of the system are grouped into classes of equivalent states). Development of CADP later moved to INRIA Grenoble, where the current group around CADP comprises Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe.
At Verimag, research continues on approaches that help design and implement safe and reliable computing systems, both on theoretical and more applied aspects. Verimag is a joint laboratory of CNRS, Université Grenoble Alpes and Grenoble-INP.
References:
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...
