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.

See also the List of case-studies published by the authors of CADP.

1990:
  1. [Networks] Bus instrumentation protocol
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. [Distributed Algorithms] Bull's Cluster File System
  2. [Business Systems] Invoicing System
  3. [Telephony] Plain Old Telephone System (POTS)
  4. [Hardware Design] CC-NUMA Cache Coherency Protocol
  5. [Communication Protocols] OM/RR Protocol for Traffic Control
  6. [Human-Computer Interaction] Multi-user Design Rationale Editor
  7. [Hardware Design] Asynchronous Circuits
  8. [Communication Protocols] INRES Protocol
  9. [Human-Computer Interaction] Formal Verification in an Interactor Model
  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

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.60 last updated on 11/12/13 12:25:33

Back to the CADP Home Page