Research Tools Connected to the CADP Toolset

Many tools are connected to the CADP toolset or even developed using the programming interfaces provided by CADP (such as the generic environments BCG and OPEN/CAESAR for enumerative and on-the-fly verification). We give here a (non-exhaustive) list of such tools, most of which have led to scientific publications.

The meaning of the icons used below is the following:
        : this page was recently added
        : this page was recently updated
        : members of the CADP team contributed to this tool development

  1. [LOTOS Tools] APERO Data Type Pre-processor for LOTOS
  2. [LOTOS Tools] ELUDO Toolkit for LOTOS
  1. [Formal Verification] FC2Tools for Verifying Transition Systems
  1. [Protocol Testing] Exploiting Symmetry in Protocol Testing
  1. [Object-Oriented Languages] BDL (Behavioural Description Language)
  2. [Protocol Testing] TorX Architecture for Test Derivation and Execution
  3. [Real-Time Systems] KRONOS-OPEN Tool for Real-Time Verification
  4. [Hardware Design] Test Generation and Execution for Synchronous Hardware
  5. [Control Systems] Timed Automata for Programmable Logic Controllers
  1. [Human-Computer Interaction] ConcurTaskTrees Environment
  2. [Formal Verification] Interaction Abstraction Algorithm
  3. [Object-Oriented Languages] UMLAUT environment for UML
  4. [B Method] Labelled Transition Systems of B specifications
  1. [Formal Verification] Implementation of the FULL Logic using XTL
  2. [Embedded Systems] CANDLE Language and Environment for CAN Control Systems
  1. [Performance Evaluation] Deriving Global Properties from Local Restrictions
  2. [Real-Time Systems] Analysis of Real-Time Systems Described in RT-LOTOS
  1. [Hardware Design] Model Checking for Systems on Chip (SoC)
  2. [Real-Time Systems] Verification of Real-Time Systems using ELSE and CADP
  3. [Telephony] Analysis of VoiceXML Interactive Voice Services
  1. [Formal Verification] On-the-Fly Interconnection of CADP and mCRL Toolsets
  2. [Bioinformatics] Model Checking Genetic Regulatory Networks using GNA and CADP
  3. [Formal Verification] Abstract Interpretation Toolkit for mCRL
  4. [Real-time UML] TTool (TURTLE Toolkit)
  1. [Web Services] Contracts and Protocols for Web Services
  2. [Asynchronous Circuits] CHP2LOTOS Translator for CHP (Communicating Hardware Processes)
  1. [Software Components] ADAPTOR Tool for Generating Software Component Adaptors
  2. [Formal Verification] VeSTA (Verification of Simulations for Timed Automata)
  3. [Static Analysis] ANNOTATOR Tool for On-the-Fly Data Flow Analysis
  4. [Software Model Checking] Model Checking C Programs using OPEN/CAESAR
  5. [Formal Verification] VERCORS Platform for Model Checking Distributed Components
  6. [Formal Verification] BFReduction and TEReduction Tools
  1. [Protocol Testing] Abstract Test Case Execution Framework
  2. [Protocol Testing] Interoperability Test Generation Algorithm
  3. [Cryptography] LYS Knowledge Analysis Toolset for Epistemic Verification
  4. [Software Components] SynthesisRT: Adaptors for Real-Time Components
  5. [Real-time Systems] MOTOR (MODEST Tool Environment)
  6. [Reliability Analysis] CORAL (COmpositional Reliability and Availability anaLysis)
  7. [Planning] Enhanced Version of ETI (Electronic Tool Integration) Platform
  8. [Grid Computing] Enhanced Version of the CRESS Tool for Analyzing Composed Grid Services
  1. [UML for Distributed Systems] CTTool for Analyzing Fractal/GCM Components with UML 2
  2. [Static Analysis] DATALOG_SOLVE Tool for Static Analysis of Object-Oriented Programs
  3. [Shared Services] COSTO Tool for Analyzing Kmelia Components and Services
  4. [Software Architecture] CHARMY and SYNTHESIS Tools for Analyzing Software Architectures
  5. [Reliability Analysis] ARCADE Framework for Architectural Dependability Evaluation
  6. [Service Protocols] DCOMPOSITOR Tool for Generating Service Wrapper Protocols
  7. [Random Testing] Random Walks for Testing
  8. [Stochastic Systems] Framework for Performance Evaluation and Functional Verification in Stochastic Process Algebras
  1. [Web Services] ITACA/ACIDE Toolbox for Composition and Adaptation of Web Services
  2. [Performance Evaluation] FLORA Framework for Software Architectures with Local Recovery
  3. [Protocol Testing] AVATR Tool for Analyzing Test Results of Océ Printers
  4. [Stochastic Systems] Performance Evaluation of Distributed Systems Based on Process Algebras
  5. [Sensor Networks] TEPAWSN Environment for the Design of Wireless Sensor Networks
  6. [Hardware Design] A SystemC/TLM Front-End for CADP
  7. [Probabilistic Systems] Support for Interactive Probabilistic Chains
  1. [Protocol Verification] LTSmin Toolset for Manipulating LTSs
  2. [Embedded Systems] Alvis Modelling Language for Embedded Systems
  3. [Protocol Testing] JTorX Tool for Model-Based Testing of Software
  4. [UML and Testing] Argos Tool for Analysing UML Descriptions
  5. [Model-Driven Engineering] Henshin Language and Toolset for Transformation of Eclipse Models
  1. [Software Components] DAMASCO Model Transformation Framework for Composition and Adaptation
  2. [Probabilistic Systems] SCOOP Tool for Symbolic Optimizations of Probabilistic Processes
  3. [Language Semantics] SLCO Language Transformation Environment
  4. [Embedded Systems] The FLAC Fiacre to LOTOS Compiler
  1. [Web Services] Formal Modeling and Validation of BPEL-based Web Service Composition
  2. [Hardware Design] Design Tool for FPGA-based Image and Video Processing
  3. [Performance Evaluation] Quantitative Timed Analysis of Interactive Markov Chains
  4. [Web Services] Synchronizability and Realizability of Asynchronous Systems
  5. [Web Services] Formal Analysis of Choreography Specifications
  6. [Learning] Automata Learning through Counterexample-guided Abstraction Refinement
  7. [Web Services] Reo Tool for Model-Checking Dataflow in Service Compositions
  8. [Software Architectures] IDCM Tool for Incremental Component-based Architectures
  9. [Reliability] DFTCalc Tool for Computing Failure Probability of Dynamic Fault Trees
  10. [Robotics] Modeling Robot Behavior with CCL
  1. [Information Systems] EB32LNT Translator from the EB3 Language to LNT
  2. [Formal Verification] PMC Tool for Compositional Verification Using Partial Model Checking
  3. [Formal Verification] REFINER Tool for Checking Property Preservation of Model Refinements
  4. [Concurrency Theory] PIC2LNT Translator from Applied Pi-Calculus to LNT
  1. [Web Services] IMCReo tool for Reasoning about QoS in Stochastic Reo Connectors
  2. [Formal Verification] ELOTON Eclipse-based Editor to Support LOTOS Newcomers
  3. [Embedded Systems] GRL2LNT Translator from GALS Representation Language to LNT
  1. [Development Tools] DLC Compiler from LNT to Distributed C Code
  2. [Software Architectures] Ocarina Tool for Analysing AADL Descriptions
  3. [Distributed Systems] The MIstRAL Tool for Middleware reconfiguration Based on Formal Methods
  4. [Formal Verification] The GROOVE Tool for Verification Based on Graph Rewriting

We are looking forward to keeping this list up to date. If you have new material to be referenced in this list, please contact

Version 1.96 last updated on 2016/09/13 16:44:32

Back to the CADP Home Page