CADP Tools Overview

The CADP toolbox contains several closely interconnected components (more than 42 tools and 17 software components), which we classify into the following categories:

  1. CADP tools for LOTOS
  2. CADP tools for explicit state space manipulation
  3. CADP tools for implicit state space manipulation
  4. CADP tools for equivalence checking
  5. CADP tools for model checking
  6. CADP tools for visual checking
  7. CADP tools for compositional verification
  8. CADP tools for distributed verification
  9. CADP tools for testing
  10. CADP tools for performance evaluation
  11. CADP user interface
  12. 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.

1. CADP tools for LOTOS

CAESAR

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

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

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

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

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

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,

  • CAESAR.OPEN, an interface with LOTOS descriptions,

  • 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.

  • 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

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

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

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

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

BCG_DRAW provides a 2-dimension graphical representation of BCG graphs with an automatic layout of states and transitions.

BCG_EDIT

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

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

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

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

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

BCG_MERGE merges the N graph fragments constructed by DISTRIBUTOR to produce the entire graph.

9. CADP tools for testing

SEQ.OPEN

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

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

BCG_MIN allows to minimize BCG graphs modulo strong or branching bisimulation, which agree with the concept of lumpability on Markov models.

CUNCTATOR

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

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

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

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.

11. CADP user interface

EUCALYPTUS

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

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

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.13 last updated on 2014/06/03 10:13:26

Back to the CADP Home Page