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] Performance Evaluation and Verification using 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
  6. [Space-mission Planning] Product-Line Approach for Families of Program Translators
  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
  5. [Distributed Systems] LFD-MPI Tool for Lightweight Formal Development of MPI Applications
  1. [Business Processes] VBPMN Tool for Checking Business Process Evolution
  2. [Web Services] Formal Specification of Web Services Composition Using LOTOS
  3. [Formal Verification] Tools and Methods for RTCP-nets Modeling and Verification
  4. [Software Architectures] Availability Analysis of Software Architecture Decomposition Alternatives
  1. [Security] Formal Analysis of Security Guidelines for Program Certification
  2. [Reliability] FTRES Tool for Rare Event Simulation in Dynamic Fault Trees
  3. [Web Services] Adaptive Service Composition based on Runtime Verification of Formal Properties
  4. [Real-time UML] The Papyrus-RT Tool for Model-driven Engineering with UML-RT
  5. [Concurrent Systems] The aZiZa Tool for Heterogeneous Behavioural Models
  6. [Reactive Systems] Formal Analysis of Distributed Reactive Applications
  7. [System Design] Debugging of Concurrent Systems using Counterexample Analysis
  8. [Process Model Analysis] Meta-Modeling Tool [εm] for Analysis of Process Models
  1. [Protocol Testing] The RichTest Tool for Message-Passing Concurrent Programs
  2. [Business Processes] MANGROVE Tool for the Analysis of Industrial Workflow-based Models
  1. [Internet of Things] IoT Composer Tool for Building and Designing IoT Applications
  1. [Internet of Things] MOZART Tool for Designing and Deploying Advanced IoT Applications
  2. [Multi-agent Systems] SLiVER Tool for Modeling and Analyzing Multi-agent Systems
  3. [System Design] Verification of Formal Requirements in the Context of ISO-26262

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.124 last updated on 2021/09/20 11:16:22

Back to the CADP Home Page