Case Studies Achieved using the CADP Toolset

The CADP toolset has been used in many different application fields. We give here a (non-exhaustive) list of case-studies, 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 case study

1989:
  1. [Networks] Alternating Bit Protocol
  2. [Hardware Design] Systolic Networks for Convolution Product
1990:
  1. [Networks] Bus Instrumentation Protocol
  2. [Telephony] Matrix Switch
1991:
  1. [Embedded Software] Car Overtaking Protocol
  2. [Cryptography] Message Authentication Algorithm (MAA, ISO 8731)
  3. [Distributed Systems] rel/REL Protocol for Reliable Atomic Multicast
  4. [Telephony] GSM Handover Procedure
1992:
  1. [Networks] OSI95 Enhanced Transport Service Specification (ETSS)
  2. [Telephony] INRES Initiator-Responder Protocol
1993:
  1. [Embedded Software] Airbus 330/340 Flight Warning Computer
1994:
  1. [Networks] "Transit Node" Message Router
  2. [Networks] Verification of an ATM Switch
  3. [Telephony] ISDN Teleservice and Call Waiting
1995:
  1. [Database Protocols] CCR (Commitment, Concurrency, and Recovery) and OSI-TP (Transaction Processing)
  2. [Telephony] Plain Ordinary Telephone Service (POTS)
  3. [Distributed Systems] Groupware Protocols
  4. [Distributed Systems] Virtual Shared Memory with Causal Coherence
1996:
  1. [Cryptography] "Equicrypt" Trusted Third Party Protocol
  2. [Embedded Software] Railyard Configurations
  3. [Communication Protocols] Philips' Bounded retransmission protocol
  4. [Networks] Internet transport protocol TCP
  5. [Telephony] Feature Interactions in Telephony Systems
  6. [Distributed Algorithms] Distributed Leader Election Algorithms for Unidirectional Ring Networks
  7. [Networks] Proactive Network Management
  8. [Hardware Design] Bus arbiter of Bull's PowerScale architecture
1997:
  1. [Database Protocols] Co4 Distributed Knowledge System
  2. [Hardware Design] Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire'')
  3. [Embedded Software] Eurocontrol's Departure Clearance protocol
  4. [Protocol Testing] Distributed Leader Election Algorithm
  5. [Hardware Design] MPI-BIP Protocol of the Myrinet High-speed Network
  6. [Software Architectures] LOTOS Patterns for Architectural Styles
1998:
  1. [Business Systems] Invoicing System
  2. [Telephony] Plain Old Telephone System (POTS)
  3. [Hardware Design] CC-NUMA Cache Coherency Protocol
  4. [Communication Protocols] OM/RR Protocol for Traffic Control
  5. [Human-Computer Interaction] Multi-user Design Rationale Editor
  6. [Hardware Design] Asynchronous Circuits
  7. [Communication Protocols] INRES Protocol
  8. [Human-Computer Interaction] Formal Verification in an Interactor Model
  9. [Distributed Algorithms] Bull's Cluster File System
  10. [Communication Protocols] Xpress Transfer Protocol (XTP)
  11. [Distributed Systems] Access control in CORBA
1999:
  1. [Communication Protocols] HAVi Leader Election Protocol
  2. [Hardware Design] Analysis of Synchronous Hardware using LOTOS
  3. [Communication Protocols] TCAP Protocol (Transaction Capabilities Procedures)
  4. [Cryptography] Challenge Handshake Authentication Protocol (CHAP)
  5. [Embedded Software] Air Traffic Control (ATC) System
  6. [Mobile Telephony] General Packet Radio Service (GPRS)
  7. [Security] SSCC (Security System against the Cloning of Cellular phones)
  8. [Hardware/Software Codesign] Hardware/Software Codesign using LOTOS
2000:
  1. [Communication Protocols] SPLICE Coordination Architecture
  2. [Embedded Software] Steam-Boiler System
  3. [Hardware Design] POLYKID CC-NUMA Multiprocessor Architecture
  4. [Software Architectures] Pipe & Filter Software Architectures
  5. [Telephony] Feature Interaction Detection
  6. [Hardware Design] Verification and Testing of Asynchronous Circuits
  7. [Protocol Testing] Conference Protocol
2001:
  1. [Distributed Algorithms] Development of a Verified Erlang Program for Resource Locking
  2. [Embedded Software] Analysis of a Distributed System for Lifting Trucks
  3. [Mobile Agents] Dynamic Reconfiguration Protocol for Agent-Based Applications
  4. [Distributed Algorithms] Formal Analysis of Checkpointing Algorithms
  5. [Communication Protocols] The Accounting Model of the TINA Architecture
  6. [Communication Protocols] Transport Layer Security Protocol
2002:
  1. [Embedded Systems] AIDA (Automatic In-Flight Data Acquisition) System
  2. [Coordination Architectures] JavaSpacesTM Shared Data Space Architecture
  3. [Cryptography] Needham-Schroeder Public Key Authentication Protocol
  4. [Coordination Architectures] Replication Features of the Splice Architecture
  5. [Software Architectures] Non-Refinement Transformations of Software Architectures
  6. [Hardware Design] SCSI-2 Bus Arbitration Protocol
  7. [Human-Computer Interaction] Object Modelling of Interactive Systems using UMLi
  8. [Radiotherapy Equipment] Testing of Electron Beam Accelerators for Radiotherapy
2003:
  1. [Communication Protocols] Positive Acknowledgement Retransmission (PAR) Protocol
  2. [Coordination Architectures] Jackal Distributed Shared Memory Implementation of Java
  3. [Coordination Architectures] Distributed Data Space Architectures Described in Space Calculus
  4. [Distributed Algorithms] Parallel Programs Developed using JavaSpacesTM
  5. [Mobile Agents] Compositional Verification of the ScalAgent Deployment Protocol
  6. [Mobile Agents] Agent-Based Dynamic Online Auction Protocol
  7. [Software Architectures] Robot Teleoperation Architecture
  8. [Communication Protocols] Pragmatic General Multicast (PGM) Protocol
  9. [Hardware Design] Asynchronous Circuit for Data Encryption Standard (DES)
  10. [Communication Protocols] Automatic Verification of the IEEE 1394 Root Contention Protocol
  11. [System on Chip] Formal Verification of the STBus Interconnect
  12. [Business Processes] Workflow Specification using LOTOS
2004:
  1. [Communication Protocols] Verification of the Chilean Electronic Invoices System
  2. [Middleware] Formalising Middleware Behaviour using LOTOS
  3. [E-commerce] Formal Verification of a Fair Payment Protocol
  4. [Web Services] Negotiation among Web Services using LOTOS/CADP
  5. [Communication Protocols] Reliable Large Scale Multipoint Transport Protocol
  6. [Industrial Manufacturing Systems] Analysis of a Turntable System
  7. [Communication Protocols] Fault-Based Testing of Concurrent Systems
2005:
  1. [Constraint Programming] Constraint Solving with LOTOS
  2. [Security Protocols] Verification of a Fair Non-Repudiation Protocol
  3. [Component-based Systems] Verification of Fractal Components
  4. [Embedded Systems] Verifying Fault-Tolerant Erlang Programs
  5. [System Security] Multilateral and RBAC Security for Management of Distributed Systems
2006:
  1. [Component-based Systems] Verification of Software Components
  2. [Embedded Systems] Automatic Document Feeder
  3. [Security Protocols] Formal Specification and Verification of a DRM Protocol
  4. [Security Protocols] Verification of Observational Determinism
  5. [Communication Protocols] Performability Evaluation of the European Train Control System
  6. [Distributed Systems] Verification of Distributed Shared Memory Systems
2007:
  1. [Hardware Design] Verification of an Asynchronous Network-on-Chip
  2. [Communication Protocols] Model-Based Testing of Registrar Entity for the Session Initiation Protocol
  3. [E-commerce] Verification of a .Net On-Line Sale Application
  4. [Cryptography] Chaum's dining cryptographers and Fujioka-Okamota-Ohta electronic voting scheme
  5. [Communication Protocols] Formal Analysis of Erlang's Open Telecom Platform Library Components
  6. [Component-based Systems] Bridge Exchanger Software Connectors for Dataflow Applications
  7. [Communication Protocols] Automatic Verification of the IEEE 1394 Tree Identify Protocol
  8. [E-Democracy] Verification of the Dutch Rijnland Internet Election System
  9. [Component-based Systems] Verification of Adaptors between Evolving Components
  10. [Embedded Systems] Analysis of Wireless Sensor Network Applications for TinyOS
2008:
  1. [Distributed Systems] Leader Election in Anonymous Ring
  2. [Distributed Systems] Analysis of First-Class Futures of Distributed Grid Components
  3. [Software Adaptation] Verification and Adaptation of WF/.NET Components
  4. [Healthcare] Abstraction and Analysis of Clinical Guidance Trees
  5. [Middleware] Specification and Verification of Middlewares
  6. [Cognitive Systems] Performance Analysis of Stimulus Rich Reactive Interfaces
  7. [Web Services] Specification and Analysis of a Web Service for GPS Navigation
  8. [Transport Safety] Model Based Importance Analysis for Minimal Cut Sets
  9. [Coordination] Formal Verification of ToolBus Scripts
  10. [Distributed Systems] Gossiping Networks
2009:
  1. [Service-Oriented Computing] Collaboration Diagrams
  2. [Industrial Manufacturing Systems] Verification of a Turntable System
  3. [Component-based Systems] Validation of Semantic Composability in Simulation Models
  4. [Distributed Algorithms] Formal Analysis of Consensus Protocols
  5. [Distributed Systems] Accelerated Heartbeat Protocols
  6. [Critical Infrastructures] Dependability and Survivability Evaluation of a Water Distribution Process
  7. [Hardware Design] Blitter Display
  8. [Communication Protocols] Trivial File Transfer Protocol
  9. [Distributed Systems] Performance Evaluation of MPI on CC-NUMA Architectures
  10. [Embedded Systems] Test Generation for Automotive Industry
  11. [Avionics] Equipment Failure Management Protocol
  12. [Avionics] Air Traffic Control Subsystem
  13. [Communication Protocols] Learnlib Framework for Extrapolating Behavioral Models
  14. [Hardware Design] Evaluation of Packet Latency on a 2D Mesh Network-on-Chip
  15. [Hardware Design] Specification and Verification of Hardware Circuits
  16. [Web Services] Automated Formal Analysis of CRESS Web and Grid Services
2010:
  1. [Telecommunications] Model-Checking Erlang
  2. [Embedded Systems] Translation Validation of (Multi-Clocked) SIGNAL Specifications
  3. [Web Services] Verification of Web Service Composition
  4. [Distributed Systems] Systematic Correct Construction of Self-Stabilizing Systems
  5. [Distributed Systems] Verification of the Behavioural Properties for Group Communications
  6. [Distributed Algorithms] Mutual Exclusion Protocols
  7. [Security Protocols] Verification of a Key Chain Based TTP Transparent CEM Protocol
  8. [Hardware Design] Scalably Verifiable Cache Coherence
  9. [Hardware Design] Validation of the xSTream Data-Flow Architecture
2011:
  1. [Security] Behavior Analysis of Malware by Rewriting-Based Abstraction
  2. [Component-based Systems] Safety Verification of Fault-Tolerant Distributed Components
  3. [Communication Protocols] Verification of Mobile Ad Hoc Networks
  4. [Embedded Systems] Semantics Tuning of UML/SysML
  5. [Trading] Atomicity Maintenance in EPCReport of ALE
  6. [Human-Computer Interaction] Rigorous Development of Prompting Dialogs
  7. [Hardware Design] Formal Analysis and Co-simulation of a Dynamic Task Dispatcher
  8. [Distributed Algorithms] SYNERGY Reconfiguration Protocol
  9. [Cloud Computing] Self-configuration Protocol for the Cloud
2012:
  1. [Communication Protocols] Learning and Testing the Bounded Retransmission Protocol
  2. [Operating Systems] Real-Time Parallel Kernel for Dependable Distributed Systems
  3. [Embedded Systems] Model Checking of Scenario-Aware Dataflow
  4. [Medical Systems] Formal Development of Control Software in the Medical Systems Domain
2013:
  1. [Component-based Systems] Hypermanager for Reconfigurable Component-Based Systems
  2. [Hardware Design] Assisting Refinement in System-on-Chip Design
  3. [Bioinformatics] Composition and Abstraction of Logical Regulatory Modules
  4. [Distributed Systems] Verification of Multiway Synchronization Protocols
  5. [Hardware Design] Formal Analysis of the ACE Cache Coherency Protocol
  6. [Hardware Design] Fault-Tolerant Routing Algorithm for a Network-on-Chip
  7. [Cloud Computing] Dynamic Management Protocol for Cloud Applications
  8. [Component-based Systems] Compatibility Checking for Asynchronous Communication
2014:
  1. [Distributed Systems] Model-based Development and Testing of a Software Bus
  2. [Security] Verification of Models Reverse Engineered from Smart-card Readers
  3. [Embedded Systems] Modeling, Verification, and Test-case Generation for the EnergyBus Standard
  4. [Human-Computer Interaction] Formal Description and Validation of Graphical User Interfaces
2015:
  1. [Software Architectures] Improving Design Pattern Finder Precision Using Model Checking
  2. [Embedded Systems] Applying Automata Learning to Embedded Control Software
  3. [Embedded Systems] Testing Autonomous Systems Using Communicating Extended FSMs
  4. [Human-Computer Interaction] Verification of Plastic User Interfaces Exploiting Domain Ontologies
  5. [Embedded Systems] Action-based Verification of a Fire Alarm System
  6. [Cryptography] Fully Asynchronous Model of the Data Encryption Standard
  7. [Distributed Systems] Formal Specification of the Raft Consensus Algorithm
  8. [Cloud Computing] Coordination of Autonomic Managers in the Cloud
2016:
  1. [Networks] Specification and Verification of TCP extended with the Window Scale Option
  2. [Concurrent Programming] Performance Evaluation of Concurrent Data Structures
  3. [Concurrent Programming] Proving Linearizability via Branching Bisimulation
  4. [Concurrency Theory] Heuristic Search for Equivalence Checking
  5. [Concurrency Theory] Computing Maximal Weak and Other Bisimulations
2017:
  1. [Manufacturing Systems] Distributed Controller for the Production Cell Benchmark
  2. [Distributed Systems] Compositional Model Checking of Liveness Properties
  3. [Robotics] Verification of Visibility-Based Properties on Multiple Moving Robots
  4. [Smart Homes] Daily-Living Activity Recognition using Model Checking
2018:
  1. [Hardware Design] Asynchronous Circuit Implementing a Memory Protection Unit
  2. [Railways] Formal Modelling and Verification of an Automatic Train Supervision System
  3. [Banking] Detection of Data Breaches in Banking Transaction Processes
  4. [Security Protocols] Formal Modeling and Analysis of the TLS Handshake Model
  5. [Distributed Systems] Experimental Analysis of Compositional State Space Generation Strategies
  6. [Component-based Systems] Model-Based Diagnosis using LNT
2019:
  1. [Internet of Things] Autonomic Resilience of Distributed IoT Applications in the Fog
  2. [Autonomous Vehicles] Probabilistic Collision Risk Estimation for Autonomous Driving
  3. [Process Mining] Model Checking Based Approach for Compliance Checking
  4. [Data Models] Finding Conservative Schema Evolutions by Analysing API Changes
  5. [Railways] Verifying Complex Software Control Systems from Test Objectives
  6. [Embedded Systems] Designing Safe Synchronous Reactive Systems
  7. [Machine Learning] Selection of Model Checking Strategies using Machine Learning
2020:
  1. [Hardware Design] Asynchronous Circuit for Protection Against Physical Attacks
  2. [Security] Detection of Android Malware using Model Checking and Machine Learning
  3. [Internet of Things] Modeling and Validation of ReDy Architecture for IoT Applications
  4. [Hardware Design] Identifying Timing Interferences on Multicore Processors
2021:
  1. [GPU Programming] Specifying and Testing GPU Workgroup Progress Models
  2. [Medical Systems] Radiomic Features for Prostate Cancer Grade Detection through Formal Verification
2022:
  1. [Autonomous Vehicles] Generation of Scenarios for Autonomous Vehicles
  2. [Object-oriented Design] Object-oriented Design Integrating Ubiquitous Specifications
  3. [Railways] Formal Modelling and Analysis of the 4SECURail Case Study
2023:
  1. [Communication Protocols] Vulnerability Identification of Operational Technology Protocols
  2. [Object-oriented Design] Verification and Validation of UML Statecharts using Process Algebra
  3. [Hardware Design] Verification of Circuits for Systolic Array Parallel Computation

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.183 last updated on 2024/04/18 15:53:17

Back to the CADP Home Page