CADP
CADP
Description: CADP ("Construction and Analysis of Distributed Processes", formerly known as "CAESAR/ALDEBARAN Development Package") is a popular toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.
Since January 2012, CADP is developed by the CONVECS team (formerly, by the VASY team). CADP is connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.
CADP offers a wide set of functionalities, ranging from step-by-step simulation to massively parallel model-checking. It is the only toolbox to offer:
Compilers for several input formalisms, e.g.:
- High-level descriptions written in various languages, such as LOTOS (ISO International Standard 8807), LNT, FSP, pi-calculus, etc. The CADP toolbox provides compilers (CAESAR, CAESAR.ADT, LNT2LOTOS, FSP2LOTOS, etc.) that translate high-level descriptions into C code to be used for simulation, verification, and testing purposes;
- Low-level descriptions specified as automata (i.e., finite state machines) and networks of communicating automata that run in parallel, synchronize, and communicate using process algebra operators or synchronization vectors.
- Several equivalence checking tools (minimization and comparisons modulo bisimulation relations), 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 together: enumerative verification, on-the-fly verification, symbolic verification using binary decision diagrams, compositional minimization, partial orders, distributed model checking, etc.
- Plus a bunch of 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.
VO Integration: No
Active: Yes
Available Benchmarks: N/A
Website: http://cadp.inria.fr/
Download: Instructions can be found here.
Documentation: User guides and publications can be fournd here.
Contact: cadp@inria.fr
Excerpt and graphic from: http://cadp.inria.fr/
Backlinks:
- Validation and Verification
- Tool
- Contact the author
- Free
- C++
- Own interface
- Own language
- Linux
- Mac OS X
- Solaris
- Windows
- Circuits
- Continuous-time Markov chains
- Discrete-Time Systems
- Nested-Unit Petri nets
- Network of timed automata
- Process calculus language: FSP
- Process calculus language: LNT
- Process calculus language: LOTOS
- Abstractions
- Bisimulation minimization
- Boolean Equation Systems
- Branching-Time Temporal Logics
- Breadth First Search Analysis
- Compositional verification
- Depth-first Search Algorithms
- Description/Modeling Language
- Distributed model checking
- Labelled Transition Systems
- Mu-Calculus
- On-the-fly model checking
- Parallel Composition
- Parameterized Boolean Equation Systems
- Probabilities on paths
- Value-passing Mu-Calculus
- Guaranteed to terminate
- Not guaranteed to terminate
- Bisimulation generation
- Description/modeling language
- Model checking
- Modeling
- Probabilistic model checking
- Reachability analysis
- Simulation
- Statistical model checking
- Visual checking