Construction and Analysis of Distributed Processes
 | This article or section is in a state of significant expansion or restructuring. You are welcome to assist in its construction by editing it as well. If this article or section has not been edited in several days, please remove this template. If you are the editor who added this template and you are actively editing, please be sure to replace this template with {{in use}} during the active editing session. Click on the link for template parameters to use.
This article was last edited by Vasywriter (talk | contribs) 15 years ago. (Update timer) |
Introduction
CADP (Construction and Analysis of Distributed Processes) formerly known as CAESAR/ALDEBARAN Development Package is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the VASY team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.
Tools summary
In this toolbox, we develop the following 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 (integers, enumerations, tuples, etc.), which are implemented optimally.
- CAESAR 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 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 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
A number of tools have been developed within the OPEN/CAESAR environment:
- BISIMULATOR, which checks bisimulation equivalences and preorders
- 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
- 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
Binary Code Graphs
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. 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 (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 steady-state numerical analysis of (extended) continuous-time Markov chains
- BCG_TRANSIENT, which performs transient numerical analysis of (extended) continuous-time Markov chains
- 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, CTL, ACTL, etc.).
- The connection between explicit models (such as BCG graphs) and implicit models (explored on the fly) is ensured by OPEN/CAESAR-compliant compilers, e.g.:
- CAESAR.OPEN, for models expressed as LOTOS descriptions
- BCG.OPEN, for models represented as BCG graphs
- EXP.OPEN, for models expressed as communicating automata
- SEQ.OPEN, for models represented as sets of execution traces
Other tools
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 project-team of \INRIA\ Rennes.
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.