CADP: A Toolbox for the Construction and Analysis of Distributed Processes

Hubert Garavel (1) , Frédéric Lang (1) , Radu Mateescu (1) , Gwen Salaün (1) , Wendelin Serwe (1)

1 CONVECS - Construction of verified concurrent systems

Asynchronous concurrency is becoming increasingly present in a large spectrum of systems, spanning from the level of systems- and networks-on-chip, over multi-processor architectures, up to the level of grid and cloud computing. Due to the intrinsic complexity of asynchronous concurrency, the correct design of such systems is notoriously difficult, requiring the support of formal methods and verification tools. CADP (Construction and Analysis of Distributed Processes) is a toolbox for the design, functional verification, and performance evaluation of asynchronous concurrent systems. Currently, CADP consists of about fifty interconnected tools and software libraries. The toolbox is distributed free of charge to academia and public research institutes, and is already used by more than 440 research institutions and companies worldwide in many application domains. Given the increasing number of systems featuring asynchronous concurrency, CADP could be used still more widely in research, industry, and education (in particular for teaching the concepts of concurrency theory). This tutorial presents the architecture and main functionalities of CADP, with a twofold objective. On the one hand, the tutorial illustrates the application of CADP to the modeling, functional verification, and performance evaluation. On the other hand, the tutorial presents various input languages accepted as input by CADP, together with software libraries that enable users to develop their own analysis tools. The well-known, but fundamental problem of mutual exclusion will serve as support to illustrate the principal functionalities of CADP: formal modeling of protocols, compositional state space generation, graph visualization, interactive step-by-step simulation, formulation and verification of temporal logic properties, as well as performance evaluation by compositional insertion of latency constraints and transformation into interactive Markov chains.

Domaines: Génie logiciel [cs.SE]; Logique en informatique [cs.LO]

Hubert Garavel, Frédéric Lang, Radu Mateescu, Gwen Salaün, Wendelin Serwe. CADP: A Toolbox for the Construction and Analysis of Distributed Processes. FM - 18th International Symposium on Formal Methods - 2012, Aug 2012, Paris, France. ⟨hal-00764932⟩