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
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)
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
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 Architecture] 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

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.151 last updated on 2018/07/20 18:15:38

Back to the CADP Home Page