Construction and Analysis of Distributed Processes
Developer(s)  INRIA CONVECS team (formerly http://vasy.inria.fr VASY] team) 

Initial release  1986, 31–32 years ago 
Stable release 
2017 / December 13, 2017

Operating system  Windows 7 and later, OS X Yosemite and later, Linux, Solaris 
Type  Toolbox for designing communication protocols and distributed systems 
Website  cadp.inria.fr 
CADP^{[1]} (Construction and Analysis of Distributed Processes) is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team (formerly by the VASY team) at INRIA RhoneAlpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.
The purpose of the CADP toolkit is to facilitate the design of reliable systems by use of formal description techniques together with software tools for simulation, rapid application development, verification, and test generation.
CADP can be applied to any system that comprises asynchronous concurrency, i.e., any system whose behavior can be modeled as a set of parallel processes governed by interleaving semantics. Therefore, CADP can be used to design hardware architecture, distributed algorithms, telecommunications protocols, etc. The enumerative verification (also known as explicit state verification) techniques implemented in CADP, though less general that theorem proving, enable an automatic, costefficient detection of design errors in complex systems.
CADP includes tools to support use of two approaches in formal methods, both of which are needed for reliable systems design:
 Models provide mathematical representations for parallel programs and related verification problems. Examples of models are automata, networks of communicating automata, Petri nets, binary decision diagrams, boolean equation systems, etc. From a theoretical point of view, research on models seeks for general results, independent of any particular description language.
 In practice, models are often too elementary to describe complex systems directly (this would be tedious and errorprone). A higher level formalism known as process algebra or process calculus is needed for this task, as well as compilers that translate highlevel descriptions into models suitable for verification algorithms.
Contents
History
Work began on CADP in 1986, when the development of the first two tools, CAESAR and ALDEBARAN, was undertaken. In 1989, the CADP acronym was coined, which stood for CAESAR/ALDEBARAN Distribution Package. Over time, several tools were added, including programming interfaces that enabled tools to be contributed: the CADP acronym then became the CAESAR/ALDEBARAN Development Package. Currently CADP contains over 50 tools. While keeping the same acronym, the name of the toolbox has been changed to better indicate its purpose: Construction and Analysis of Distributed Processes.
Major releases
The releases of CADP have been successively named with alphabetic letters (from "A" to "Z"), then with the names of cities hosting academic research groups actively working on the LOTOS language and, more generally, the names of cities in which major contributions to concurrency theory have been made.
Code name  Date 

"A" ... "Z"  January 1990  December 1996 
Twente  June 1997 
Liege  January 1999 
Ottawa  July 2001 
Edinburgh  December 2006 
Zurich  December 2013 
Amsterdam  December 2014 
Stony Brook  December 2015 
Oxford  December 2016 
Sophia Antipolis  December 2017 
Between major releases, minor releases are often available, providing early access to new features and improvements. For more information, see the change list page on the CADP website.
CADP features
CADP offers a wide set of functionalities, ranging from stepbystep simulation to massively parallel model checking. It includes:
 Compilers for several input formalisms:
 Highlevel protocol descriptions written in the ISO language LOTOS.^{[2]} The toolbox contains two compilers (CAESAR and CAESAR.ADT) that translate LOTOS descriptions into C code to be used for simulation, verification, and testing purposes.
 Lowlevel protocol descriptions specified as finite state machines.
 Networks of communicating automata, i.e., finite state machines running in parallel and synchronized (either using process algebra operators or synchronization vectors).
 Several equivalence checking tools (minimization and comparisons modulo bisimulation relations), such as BCG_MIN and BISIMULATOR.
 Several modelcheckers for various temporal logic and mucalculus, such as EVALUATOR and XTL.
 Several verification algorithms combined: enumerative verification, onthefly verification, symbolic verification using binary decision diagrams, compositional minimization, partial orders, distributed model checking, etc.
 Plus other tools with advanced functionalities such as visual checking, performance evaluation, etc.
CADP is designed in a modular way and puts the emphasis on intermediate formats and programming interfaces (such as the BCG and OPEN/CAESAR software environments), which allow the CADP tools to be combined with other tools and adapted to various specification languages.
Models and verification techniques
Verification is comparison of a complex system against a set of properties characterizing the intended functioning of the system (for instance, deadlock freedom, mutual exclusion, fairness, etc.).
Most of the verification algorithms in CADP are based on the labeled transition systems (or, simply, automata or graphs) model, which consists of a set of states, an initial state, and a transition relation between states. This model is often generated automatically from high level descriptions of the system under study, then compared against the system properties using various decision procedures. Depending on the formalism used to express the properties, two approaches are possible:
 Behavioral properties express the intended functioning of the system in the form of automata (or higher level descriptions, which are then translated into automata). In such a case, the natural approach to verification is equivalence checking, which consists in comparing the system model and its properties (both represented as automata) modulo some equivalence or preorder relation. CADP contains equivalence checking tools that compare and minimize automata modulo various equivalence and preorder relations; some of these tools also apply to stochastic and probabilistic models (such as Markov chains). CADP also contains visual checking tools that can be used to verify a graphical representation of the system.
 Logical properties express the intended functioning of the system in the form of temporal logic formulas. In such a case, the natural approach to verification is model checking, which consists of deciding whether or not the system model satisfies the logical properties. CADP contains model checking tools for a powerful form of temporal logic, the modal mucalculus, which is extended with typed variables and expressions so as to express predicates over the data contained in the model. This extension provides for properties that could not be expressed in the standard mucalculus (for instance, the fact that the value of a given variable is always increasing along any execution path).
Although these techniques are efficient and automated, their main limitation is the state explosion problem, which occurs when models are too large to fit in computer memory. CADP provides software technologies for handling models in two complementary ways:
 Small models can be represented explicitly, by storing in memory all their states and transitions (exhaustive verification);
 Larger models are represented implicitly, by exploring only the model states and transitions needed for the verification (on the fly verification).
Languages and compilation techniques
Accurate specification of reliable, complex systems requires a language that is executable (for enumerative verification) and has formal semantics (to avoid any as language ambiguities that could lead to interpretation divergences between designers and implementors). Formal semantics are also required when it is necessary to establish the correctness of an infinite system; this cannot be done using enumerative techniques because they deal only with finite abstractions, so must be done using theorem proving techniques, which only apply to languages with a formal semantics.
CADP acts on a LOTOS description of the system. LOTOS is an international standard for protocol description (ISO/IEC standard 8807:1989), which combines the concepts of process algebras (in particular CCS and CSP and algebraic abstract data types. Thus, LOTOS can describe both asynchronous concurrent processes and complex data structures.
LOTOS was heavily revised in 2001, leading to the publication of ELOTOS (EnhancedLotos, ISO/IEC standard 15437:2001), which tries to provide a greater expressiveness (for instance, by introducing quantitative time to describe systems with realtime constraints) together with a better user friendliness.
Several tools exist to convert descriptions in other process calculi or intermediate format into LOTOS, so that the CADP tools can then be used for verification.
Licensing and installation
CADP is distributed free of charge to universities and public research centers. Users in industry can obtain an evaluation license for noncommercial use during a limited period of time, after which a full license is required. To request a copy of CADP, complete the registration form at.^{[3]} After the license agreement has been signed, you will receive details of how to download and install CADP.
Tools summary
The toolbox contains several tools:
 CAESAR.ADT^{[4]} is a compiler that translates LOTOS abstract data types into C types and C functions. The translation involves patternmatching compiling techniques and automatic recognition of usual types (integers, enumerations, tuples, etc.), which are implemented optimally.
 CAESAR^{[5]} is a compiler that translates LOTOS processes into either C code (for rapid prototyping and testing purposes) or finite graphs (for verification). The translation is done using several intermediate steps, among which the construction of a Petri net extended with typed variables, data handling features, and atomic transitions.
 OPEN/CAESAR^{[6]} is a generic software environment for developing tools that explore graphs on the fly (for instance, simulation, verification, and test generation tools). Such tools can be developed independently of any particular high level language. In this respect, OPEN/CAESAR plays a central role in CADP by connecting languageoriented tools with modeloriented tools. OPEN/CAESAR consists of a set of 16 code libraries with their programming interfaces, such as:
 Caesar_Hash, which contains several hash functions
 Caesar_Solve, which resolves boolean equation systems on the fly
 Caesar_Stack, which implements stacks for depthfirst search exploration
 Caesar_Table, which handles tables of states, transitions, labels, etc.
A number of tools have been developed within the OPEN/CAESAR environment:

 BISIMULATOR, which checks bisimulation equivalences and preorders
 CUNCTATOR, which performs onthefly steady state simulation
 DETERMINATOR, which eliminates stochastic nondeterminism in normal, probabilistic, or stochastic systems
 DISTRIBUTOR, which generates the graph of reachable states using several machines
 EVALUATOR, which evaluates regular alternationfree mucalculus formulas
 EXECUTOR, which performs random execution of code
 EXHIBITOR, which searches for execution sequences matching a given regular expression
 GENERATOR, which constructs the graph of reachable states
 PREDICTOR, which predict the feasibility of reachability analysis,
 PROJECTOR, which computes abstractions of communicating systems
 REDUCTOR, which constructs and minimizes the graph of reachable states modulo various equivalence relations
 SIMULATOR, XSIMULATOR and OCIS, which allow interactive simulation
 TERMINATOR, which searches for deadlock states
 BCG (Binary Coded Graphs) is both a file format for storing very large graphs on disk (using efficient compression techniques) and a software environment for handling this format, including partitioning graphs for distributed processing. BCG also plays a key role in CADP as many tools rely on this format for their inputs/outputs. The BCG environment consists of various libraries with their programming interfaces, and of several tools, including:
 BCG_DRAW, which builds a twodimensional view of a graph,
 BCG_EDIT which allows to modify interactively the graph layout produced by Bcg_Draw
 BCG_GRAPH, which generates various forms of practically useful graphs
 BCG_INFO, which displays various statistical information about a graph
 BCG_IO, which performs conversions between BCG and many other graph formats
 BCG_LABELS, which hides and/or renames (using regular expressions) the transition labels of a graph
 BCG_MERGE, which gathers graph fragments obtained from distributed graph construction
 BCG_MIN, which minimizes a graph modulo strong or branching equivalences (and can also deal with probabilistic and stochastic systems)
 BCG_STEADY, which performs steadystate numerical analysis of (extended) continuoustime Markov chains
 BCG_TRANSIENT, which performs transient numerical analysis of (extended) continuoustime Markov chains
 PBG_CP, which copies a partitioned BCG graph
 PBG_INFO, which displays information about a partitioned BCG graph
 PBG_MV which moves a partitioned BCG graph
 PBG_RM, which removes a partitioned BCG graph
 XTL (eXecutable Temporal Language), which is a high level, functional language for programming exploration algorithms on BCG graphs. XTL provides primitives to handle states, transitions, labels, successor and predecessor functions, etc. For instance, one can define recursive functions on sets of states, which allow to specify in XTL evaluation and diagnostic generation fixed point algorithms for usual temporal logics (such as HML,^{[7]} CTL,^{[8]} ACTL,^{[9]} etc.).
The connection between explicit models (such as BCG graphs) and implicit models (explored on the fly) is ensured by OPEN/CAESARcompliant compilers including:

 CAESAR.OPEN, for models expressed as LOTOS descriptions
 BCG.OPEN, for models represented as BCG graphs
 EXP.OPEN, for models expressed as communicating automata
 FSP.OPEN, for models expressed as FSP descriptions
 LNT.OPEN, for models expressed as LNT descriptions
 SEQ.OPEN, for models represented as sets of execution traces
The CADP toolbox also includes additional tools, such as ALDEBARAN and TGV (Test Generation based on Verification) developed by the Verimag laboratory (Grenoble) and the Vertecs projectteam of INRIA Rennes.
The CADP tools are wellintegrated and can be accessed easily using either the EUCALYPTUS graphical interface or the SVL^{[10]} scripting language. Both EUCALYPTUS and SVL provide users with an easy, uniform access to the CADP tools by performing file format conversions automatically whenever needed and by supplying appropriate commandline options as the tools are invoked.
See also
References
 ^ Garavel H, Lang F, Mateescu R, Serwe W: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes International Journal on Software Tools for Technology Transfer (STTT), 15(2):89107, April 2013
 ^ ISO 8807, Language of Temporal Ordering Specification
 ^ CADP Online Request Form. Cadp.inria.fr (20110830). Retrieved on 20140616.
 ^ H. Garavel. Compilation of LOTOS Abstract Data Types, in Proceedings of the 2nd International Conference on Formal Description Techniques FORTE'89 (Vancouver B.C., Canada), S. T. Vuong (editor), NorthHolland, December 1989, p. 147–162.
 ^ H. Garavel, J. Sifakis. Compilation and Verification of LOTOS Specifications, in Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), L. Logrippo, R. L. Probert, H. Ural (editors), NorthHolland, IFIP, June 1990, p. 379–394.
 ^ H. Garavel. OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing, in Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98 (Lisbon, Portugal), Berlin, B. Steffen (editor), Lecture Notes in Computer Science, Full version available as Inria Research Report RR3352, Springer Verlag, March 1998, vol. 1384, p. 68–84.
 ^ M. Hennessy, R. Milner. Algebraic Laws for Nondeterminism and Concurrency, in: Journal of the ACM, 1985, vol. 32, p. 137–161.
 ^ E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatic Verification of FiniteState Concurrent Systems using Temporal Logic Specifications, in: ACM Transactions on Programming Languages and Systems, April 1986, vol. 8, no 2, p. 244–263.
 ^ R. De Nicola, F. W. Vaandrager. Action versus State Based Logics for Transition Systems, Lecture Notes in Computer Science, Springer Verlag, 1990, vol. 469, p. 407–419.
 ^ H. Garavel, F. Lang. SVL: a Scripting Language for Compositional Verification, in: Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001 (Cheju Island, Korea), M. Kim, B. Chin, S. Kang, D. Lee (editors), Full version available as Inria Research Report RR4223, Kluwer Academic Publishers, IFIP, August 2001, p. 377–392.
External links
 http://cadp.inria.fr/
 http://vasy.inria.fr/
 http://convecs.inria.fr/