The CADP toolbox contains several closely interconnected components (more than 42 tools and 17 software components), which we classify into the following categories:
- CADP tools for LOTOS
- CADP tools for explicit state space manipulation
- CADP tools for implicit state space manipulation
- CADP tools for equivalence checking
- CADP tools for model checking
- CADP tools for visual checking
- CADP tools for compositional verification
- CADP tools for distributed verification
- CADP tools for testing
- CADP tools for performance evaluation
- CADP user interface
- CADP installation and maintenance tools
There exist other tools interconnected with the CADP toolbox. See the list of research tools developed using CADP for details.
-
-
CAESAR is a compiler that translates the behavioural part of a LOTOS
specification into either a C program (to be executed or simulated)
or into an LTS (to be verified using bisimulation tools and/or temporal
logic evaluators).
For instance, one can check the LTS of a protocol against the
LTS of the service implemented by the protocol. Both LTSs are
generated using CAESAR and compared using BISIMULATOR. It is
also possible to specify protocol properties using temporal
logic formulas that can be evaluated on the protocol LTS.
CAESAR translation algorithms proceed in several steps.
First the LOTOS description is translated into a simplified
process algebra called SUBLOTOS. Then an intermediate Petri
Net model is generated, which provides a compact, structured
and user-readable representation of both the control and
data flow. Eventually the LTS is produced by performing
reachability analysis on the Petri net.
CAESAR accepts full LOTOS with the following restriction as
regards the control part: process recursion is not allowed
on the left and right hand part of |[...]|, nor on the left
hand part of >> and [>. Despite these restrictions, the
subset of LOTOS handled by CAESAR is large and usually
sufficient for real-life needs.
The current version of CAESAR allows the generation of large
LTSs (some million states) within a reasonable lapse of
time. Moreover, the efficient compiling algorithms of CAESAR
can also be exploited in the framework of the OPEN/CAESAR
environment (see below).
The most recent version of CAESAR provides a functionality
called EXEC/CAESAR for C code generation. This C code
interfaces with the real world, and can be embedded in
applications. This allows rapid prototyping directly from the
LOTOS specification.
-
-
CAESAR.ADT is a compiler that translates the data part of
LOTOS specifications into libraries of C types and functions.
Each LOTOS sort is translated into an equivalent C type and
each LOTOS operation is translated into an equivalent C
function (or macro-definition). CAESAR.ADT also generates C
functions for comparing and printing abstract data types
values, as well as iterators for the sorts the domain of
which is finite.
One must indicate to CAESAR.ADT which LOTOS operations are
``constructors'' and which are not (fairly obvious, in
practice). CAESAR.ADT does not allow non-free constructors
(``equations between constructors''). However, it is always
possible to transform a LOTOS specification in order to remove
equations between constructors.
CAESAR.ADT accepts fulls LOTOS with the following restriction,
as regards the data part: so-called "constructor discipline"
has to be enforced: constructor operations must be identified;
equations are oriented; there is a decreasing priority between
equations; equations between constructors are not allowed.
Also, parametrized types are not compiled (yet).
CAESAR.ADT is fast: translation of large programs (several
hundreds of lines) is usually achieved in a few seconds.
CAESAR.ADT can be used in conjunction with CAESAR, but it can
also be used separately to compile and execute efficiently
large abstract data types descriptions.
-
-
CAESAR.BDD performs structural analysis of hierarchical Petri
nets using Binary Decision Diagrams. It is used in particular
to perform optimizations on the intermediate Petri net
generated by CAESAR.
-
-
CAESAR.INDENT is a LOTOS program formatter. It checks first the
syntax of the LOTOS description and then indents it in a way
that makes reading it easy.
|
2. CADP tools for explicit state space manipulation
|
-
-
BCG (Binary-Coded Graphs) is both a format for the
representation of explicit LTSs and a collection of libraries
and programs dealing with this format. Compared to ASCII-based
formats for LTSs, the BCG format uses a binary representation
with compression techniques resulting in much smaller (up to
20 times) files. BCG is independent from any source language
but keeps track of the objects (types, functions, variables)
defined in the source programs.
The following tools are currently available for this format:
-
BCG_DRAW
provides a graphical representation of BCG graphs,
-
BCG_EDIT
is an interactive editor which allows to modify
manually the display generated by BCG_DRAW,
-
BCG_GRAPH
allows to generate various kinds of graphs, such as
FIFO buffers, bag buffers, and chaos automata,
-
BCG_INFO
provides information about BCG graphs such as the
size of the graph, its number of states and
transitions, the list of its labels, etc.,
-
BCG_IO
performs conversions between the BCG format
and a dozen of other formats,
-
BCG_LABELS
allows to hide and/or rename the labels of a
graph according to regular expressions,
-
BCG_LIB
generates dynamic libraries for BCG graphs,
-
BCG_MIN
minimizes graphs according to strong or branching
bisimulation (including the case of stochastic and
probabilistic systems),
-
BCG_OPEN
establishes a gateway between the BCG format
and the OPEN/CAESAR environment,
-
BCG_STEADY
performs steady-state analysis on a Markov chain
represented as a BCG graph,
-
BCG_TRANSIENT
performs transient analysis on a Markov chain
represented as a BCG graph.
Moreover, two simple application programming interfaces named
BCG_READ
and
BCG_WRITE
are available, respectively to read and to produce a BCG graph.
|
3. CADP tools for implicit state space manipulation
|
-
-
OPEN/CAESAR is an extensible, language-independent environment
that allows user-defined programs for simulation,
execution, verification (partial, on-the-fly, etc.), and test
generation to be developed in a simple and modular way.
Various modules have already been written in the OPEN/CAESAR
framework, including:
-
OCIS,
XSIMULATOR,
and
SIMULATOR,
three interactive simulators (with shell-like and X-window
interfaces),
-
EXECUTOR,
a random execution tool,
-
TERMINATOR,
a deadlock detection tool based on G. Holzmann's technique,
-
GENERATOR
and
REDUCTOR,
two reachability analysis tools, the latter being combined with
on-the-fly reduction modulo various relations,
-
PREDICTOR,
a tool to predict the feasability of reachability analysis,
-
EXHIBITOR,
a sequence-searching tool,
-
PROJECTOR,
a tool for abstracting an LTS w.r.t. an interface,
-
BISIMULATOR,
a tool for comparing two LTSs modulo a given equivalence or
preorder relation,
-
EVALUATOR,
an on-the-fly model-checker for regular alternation-free mu-calculus
formulas on Labelled Transition Systems,
-
TGV,
a tool for the generation of conformance test suites based on verification technology.
Six languages have access to the OPEN/CAESAR environment,
via the following tools:
-
BCG_OPEN,
an interface with the BCG graph format,
-
EXP.OPEN,
an interface with systems of communicating automata in the EXP
format,
-
FSP.OPEN,
an interface with FSP descriptions.
-
LNT.OPEN,
an interface with LNT descriptions.
-
LOTOS.OPEN,
an interface with LOTOS descriptions,
-
SEQ.OPEN,
an interface with sets of traces encoded in the SEQUENCE
format.
Since OPEN/CAESAR is open and well-documented, users can
easily extend the environment by adding their own modules to
fit specific needs.
|
4. CADP tools for equivalence checking
|
-
-
BISIMULATOR is an equivalence checker, which takes as input two graphs
to be compared (one represented implicitly using the OPEN/CAESAR
environment, the other represented explicitly as a BCG file) and
determines whether they are equivalent (modulo a given equivalence
relation) or whether one of them is included in the other (modulo a
given preorder relation). BISIMULATOR works on the fly, meaning that
only those parts of the implicit graph pertinent to verification are
explored. Due to the use of OPEN/CAESAR, BISIMULATOR can be applied
directly to descriptions written in high level languages (for instance,
LOTOS). This is a significant improvement compared to older tools
(such as ALDEBARAN and FC2IMPLICIT) which only accepted lower level
models (networks of communicating automata).
BISIMULATOR works by reformulating the graph comparison problem in
terms of a boolean equation system, which is solved on the fly using
the CAESAR_SOLVE library. A useful functionality of BISIMULATOR is the
generation of a ``negative'' diagnostic (i.e., a counterexample), which
explains why two graphs are not equivalent (or not included one in the
other). The diagnostics generated by BISIMULATOR are directed acyclic
graphs and are usually much smaller than those generated by other tools
(such as ALDEBARAN), which can only generate counterexamples restricted
to sets of traces.
-
-
REDUCTOR is a reachability analysis tool combined with on-the-fly
reduction modulo various relations. It operates on graphs represented
implicitly using the OPEN/CAESAR environment and provides eight
reduction algorithms:
- It can eliminate both tau-transitions and the so-called
redundant transitions, still preserving safety equivalence.
- It can eliminate all tau-transitions, still preserving tau*.a
equivalence.
- It can eliminate all circuits of tau-transitions, still
preserving branching equivalence (this reduction is called
tau-compression).
- It can perform tau-confluence reduction, still preserving
branching equivalence.
- It can eliminate duplicate transitions, still preserving strong
equivalence.
- It can determinize the graph, still preserving trace
equivalence.
- It can both eliminate tau-transitions and determinize the graph,
still preserving weak trace equivalence.
- It can fully minimize the graph modulo strong equivalence.
The 1st, 4th, and 8th reductions above are obtained by encoding the
reduction problem into a boolean equation system that is resolved on
the fly using the CAESAR_SOLVE library. The 8th reduction is
``orthogonal'' with the first five reductions in the sense that it can
be combined with any of them.
|
5. CADP tools for model checking
|
-
-
EVALUATOR is an on-the-fly model-checker for regular alternation-free
mu-calculus formulas on Labelled Transition Systems. The input language
of EVALUATOR is an extension of the alternation-free mu-calculus with
boolean formulas over actions and regular expressions over action
sequences, allowing a simple, compact specification of safety,
liveness, and fairness properties. The input language is extensible,
due to a macro-expansion and a file inclusion mechanism, which allows
to define reusable libraries of new temporal operators.
The model-checking algorithms of EVALUATOR are based on the efficient
local resolution of boolean equation systems. EVALUATOR is equipped
with diagnostic generation algorithms, which construct both examples
and counterexamples (i.e., portions of LTS explaining why a formula
is true or false).
-
-
XTL (eXecutable Temporal Language) is a functional-like programming language
designed to allow an easy, compact implementation of various temporal
logic operators. These operators are evaluated over an LTS encoded in
the BCG format. Besides the usual predefined types (booleans,
integers, etc.), the XTL language defines special types, such as sets of
states, transitions, and labels of the LTS. It offers primitives to
access the informations contained in states and labels, to obtain the
initial state, and to compute the successors and predecessors of states
and transitions. The temporal operators can be easily implemented
using these functions together with recursive user-defined functions
working with sets of states and/or transitions of the LTS.
A prototype compiler for XTL has been developed, and several temporal
logics like HML, CTL, ACTL and LTAC have been easily implemented in XTL.
|
6. CADP tools for visual checking
|
-
-
BCG_DRAW provides a 2-dimension graphical representation of BCG graphs
with an automatic layout of states and transitions.
-
-
BCG_EDIT is an interactive editor which allows to modify manually the
display generated by BCG_DRAW.
|
7. CADP tools for compositional verification
|
-
-
EXP.OPEN is a tool that explores on the fly the graph corresponding to
a network of communicating automata (represented as a set of BCG
files). These automata are composed together in parallel using either
algebraic operators (as in CCS, CSP, LOTOS, and muCRL), ``graphical''
operators (as in E-LOTOS and LNT), or synchronization vectors (as
in the MEC and FC2 tools). Additional operators are available to hide
and/or rename labels (using regular expressions) and to cut certain
transitions.
-
-
PROJECTOR is a tool that abstracts the behaviour of an OPEN/CAESAR
graph by taking into account interface constraints represented as a
BCG graph and a set of synchronization labels. The result is a BCG
graph which consists of the states and transitions of the input
OPEN/CAESAR graph that are reachable when computing the product of
the input OPEN/CAESAR graph with the interface, synchronized on the
given set of synchronization labels.
-
-
SVL (Script Verification Language) is a scripting language that targets
at simplifying and automating the verification of LOTOS programs.
SVL behaves as a tool-independent coordination language on top of
CADP, in the same way as EUCALYPTUS is a tool-independent graphical
user interface.
SVL offers high-level operators for generation, parallel composition,
minimization, label hiding, label renaming, abstraction, comparison,
and model-checking of LTSs. It supports several methods of verification
(e.g., enumerative, compositional, and on-the-fly), which can be easily
combined together.
A compiler for SVL has been developed, which translates an SVL
verification scenario into a Bourne shell script, which will perform
all the operations needed to execute the verification scenario, e.g.,
invoking verification tools with appropriate options and parameters,
generating intermediate files, etc.
SVL has been used in several case-studies: most of the CADP demo
examples take advantage of SVL readability and conciseness.
|
8. CADP tools for distributed verification
|
To push forward the limits of enumerative verification algorithms, CADP
includes tools to parallelize the graph construction algorithm, which can
be used on clusters of PCs and networks of workstations.
-
-
DISTRIBUTOR splits the construction of a graph over N machines
communicating using Tcp/Ip sockets. Each machine builds a graph
fragment, the distribution of states between the machines being
determined by a static hash function.
-
-
BCG_MERGE merges the N graph fragments constructed by DISTRIBUTOR to
produce the entire graph.
|
9. CADP tools for testing
|
-
-
SEQ.OPEN is a tool which allows to verify execution traces generated
by a system functioning as a black-box automatically. SEQ.OPEN
allows to use the verification tools developed in the OPEN/CAESAR
environment to work on traces encoded in the SEQ format. SEQ.OPEN
does not load the execution traces in memory, which allows to verify
very long traces, and uses a software cache to optimize access to
frequently visited transitions and labels.
-
-
TGV is a tool for the generation of conformance test suites based on
verification technology (jointly developed by the PAMPA team of INRIA
Rennes and the Verimag laboratory and integrated into the CADP toolbox
with the help of the VASY team). TGV takes as entries a description of
a protocol's behaviour and a test purpose, which selects the subset of
the protocol's behaviour to be tested. It produces test suites, which
are used to assess the conformance of a protocol implementation with
respect to the formal specification of the protocol.
|
10. CADP tools for performance evaluation
|
The BCG graph format allows to represent graphs consisting of a
combination of normal transitions, probabilistic transitions, and
stochastic transitions. Thus, the BCG graph format allows to encode
several kinds of (discrete or continuous time) Markov models, which
can be used to analyse the performance of a system. CADP contains
several tools which allow to analyse such graphs.
-
-
BCG_MIN allows to minimize BCG graphs modulo strong or branching
bisimulation, which agree with the concept of lumpability on
Markov models.
-
-
CUNCTATOR takes as input a Continuous Time Markov Chain expressed
as an implicit OPEN/CAESAR graph, performs an on-the-fly
steady-state simulation whose termination is specified by a maximal
virtual time elapsed or by a maximal number of transitions explored,
and outputs the equilibrium throughputs for a given set of actions.
-
-
DETERMINATOR takes as input a Markov model expressed as an implicit
OPEN/CAESAR graph, checks that it satisfies certain conditions and,
if so, generates a reduced Continuous Time Markov Chain in the BCG
format by removing stochastic nondeterminism on-the-fly.
-
-
BCG_STEADY performs steady-state analysis on a Continuous Time Markov
Chain encoded in the BCG format. It computes the equilibrium
(steady-state) probability distribution on the long run using
the Gauss/Seidel algorithm and can also compute throughputs for the
transitions of the system.
-
-
BCG_TRANSIENT performs transient analysis on a Continuous Time Markov
Chain encoded in the BCG format. It computes the time-dependent
(transient) probability distribution of the model at several
(user-specified) time instants using the uniformization algorithm and
the Fox-Glynn method to approximate Poisson probabilities and can also
compute throughputs for the transitions of the system.
-
-
EUCALYPTUS is a graphical user interface written in Tcl/Tk
that integrates CADP and several other tools developed
(APERO (Liege, Belgium), ELUDO (Ottawa, Canada),
FC2TOOLS (Sophia-Antipolis, France),
VISCOPE (Rennes, France)) in a unified, user-friendly interface.
This interface has the name of the project within which it was
developed: the euro-canadian project
"
EUCALYPTUS"
|
12. CADP installation and maintenance tools
|
-
-
INSTALLATOR is CADP's installation assistant. It makes CADP's
installation really easy and trouble-free. It checks for the
latest version of CADP and installs it on your machine.
-
-
TST is a tool which checks the way CADP is installed and configured
on the current machine in order to detect potential problems. Many
verifications are performed, most of which derived from common
problems reported by CADP users.
Version 2.18 last updated on 2020/02/12 11:50:49
Back to the CADP Home Page
