Construction and Analysis of Distributed Processes
CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes 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 techniques implemented in CADP, though less general that theorem proving, enable an automatic, cost-efficient 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. A higher level formalism known as process algebra or process calculus is needed for this task, as well as compilers that translate high-level descriptions into models suitable for verification algorithms.
History
Construction and Analysis of Distributed Processes.
Major releases
The releases of CADP have been successively named with alphabetic letters, 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 |
| Uppsala | December 2018 |
| Pisa | December 2019 |
Between major releases, minor releases are often available, providing early access to new features and improvements. For more information, see the page on the CADP website.
CADP features
CADP offers a wide set of functionalities, ranging from step-by-step simulation to massively parallel model checking. It includes:- Compilers for several input formalisms:
- * High-level protocol descriptions written in the ISO language LOTOS. The toolbox contains two compilers that translate LOTOS descriptions into C code to be used for simulation, verification, and testing purposes.
- * Low-level protocol descriptions specified as finite state machines.
- * Networks of communicating automata, i.e., finite state machines running in parallel and synchronized.
- Several equivalence checking tools, such as BCG_MIN and BISIMULATOR.
- Several model-checkers for various temporal logic and mu-calculus, such as EVALUATOR and XTL.
- Several verification algorithms combined: enumerative verification, on-the-fly 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.
Models and verification techniques
Verification is comparison of a complex system against a set of properties characterizing the intended functioning of the system.Most of the verification algorithms in CADP are based on the labeled transition systems 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. In such a case, the natural approach to verification is equivalence checking, which consists in comparing the system model and its properties 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. 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 mu-calculus, 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 mu-calculus.
- Small models can be represented explicitly, by storing in memory all their states and transitions ;
- Larger models are represented implicitly, by exploring only the model states and transitions needed for the verification.
Languages and compilation techniques
CADP acts on a LOTOS description of the system. LOTOS is an international standard for protocol description, which combines the concepts of process algebras, which tries to provide a greater expressiveness 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 non-commercial 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. 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 is a compiler that translates LOTOS abstract data types into C types and C functions. The translation involves pattern-matching compiling techniques and automatic recognition of usual types, which are implemented optimally.
- CAESAR is a compiler that translates LOTOS processes into either C code or finite graphs. 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 is a generic software environment for developing tools that explore graphs on the fly. 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 language-oriented tools with model-oriented 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 depth-first search exploration
- * Caesar_Table, which handles tables of states, transitions, labels, etc.
- * BISIMULATOR, which checks bisimulation equivalences and preorders
- * CUNCTATOR, which performs on-the-fly 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 alternation-free mu-calculus 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, X-SIMULATOR and OCIS, which allow interactive simulation
- * TERMINATOR, which searches for deadlock states
- BCG is both a file format for storing very large graphs on disk 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 two-dimensional 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 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
- * BCG_STEADY, which performs steady-state numerical analysis of continuous-time Markov chains
- * BCG_TRANSIENT, which performs transient numerical analysis of continuous-time 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, 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.
- * 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 tools are well-integrated and can be accessed easily using either the EUCALYPTUS graphical interface or the SVL 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 command-line options as the tools are invoked.