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

1996:
  1. [LOTOS Tools] APERO Data Type Pre-processor for LOTOS
  2. [LOTOS Tools] ELUDO Toolkit for LOTOS
1997:
  1. [Formal Verification] FC2Tools for Verifying Transition Systems
1998:
  1. [Protocol Testing] Exploiting Symmetry in Protocol Testing
1999:
  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
2000:
  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
2001:
  1. [Formal Verification] Implementation of the FULL Logic using XTL
  2. [Embedded Systems] CANDLE Language and Environment for CAN Control Systems
2002:
  1. [Performance Evaluation] Deriving Global Properties from Local Restrictions
  2. [Real-Time Systems] Analysis of Real-Time Systems Described in RT-LOTOS
2003:
  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
2004:
  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)
2005:
  1. [Web Services] Contracts and Protocols for Web Services
  2. [Asynchronous Circuits] CHP2LOTOS Translator for CHP (Communicating Hardware Processes)
2006:
  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
2007:
  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
2008:
  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 Architectures] 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
2009:
  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] TLM.open: A SystemC/TLM Front-End for CADP
  7. [Probabilistic Systems] Support for Interactive Probabilistic Chains
2010:
  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
2011:
  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
2012:
  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 Analysis] DFTCalc Tool for Computing Failure Probability of Dynamic Fault Trees
  10. [Robotics] Modeling Robot Behavior with CCL
2013:
  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
2014:
  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
2015:
  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
2016:
  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
2017:
  1. [Security] Formal Analysis of Security Guidelines for Program Certification
  2. [Reliability Analysis] 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
2018:
  1. [Protocol Testing] The RichTest Tool for Message-Passing Concurrent Programs
  2. [Business Processes] MANGROVE Tool for the Analysis of Industrial Workflow-based Models
2019:
  1. [Internet of Things] IoT Composer Tool for Building and Designing IoT Applications
2020:
  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
2021:
  1. [Debugging] Debugging and Verification Tools for LINGUA FRANCA in GEMOC Studio
  2. [Embedded Systems] Explaining Safety Violations in Real-Time Systems
  3. [System Design] Quantifying the Similarity of Non-bisimilar Labelled Transition Systems
  4. [Concurrent Systems] Accelerating the Computation of Dead and Concurrent Places using Reductions
2022:
  1. [Industrial Internet of Things] Probabilistic Analysis of Industrial IoT Applications
  2. [Business Processes] Probabilistic Model Checking of BPMN Processes at Runtime
2023:
  1. [Object-Oriented Languages] UML Model Checker

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

Version 1.133 last updated on 2024/03/19 17:32:16

Back to the CADP Home Page