Showcases

From MCRL2

This page provides a by no means complete list of Case Studies and Examples where mCRL2 or μCRL were used.

• AIA ITP load-balancer
• Atacama Large Millimeter Array
• Automated parking garage
• Automatic document feeder
• Control Software of the CMS Experiment at CERN's Large Hadron Collider
• Distributed system for lifting trucks
• Generic driving actuator
• IEEE 1394 link layer
• LedSync communication protocol
• Pacemaker
• Patient support platform
• PCB Printer
• Dogfooding the structural operational semantics of mCRL2

A number of case studies also made use of the CADP toolset, mainly for model-checking μ-calculus formulae and visualization purposes. On the list of case studies done with CADP toolset one finds the following descriptions of such cases:

• 41: TCAP Protocol (Transaction Capabilities Procedures) [1]
• 47: SPLICE Coordination Architecture [2]
• 54: Development of a Verified Erlang Program for Resource Locking [3]
• 60: AIDA (Automatic In-Flight Data Acquisition) System [4]
• 61: JavaSpaces (TM) Shared Data Space Architecture [5]
• 62: Needham-Schroeder Public Key Authentication Protocol [6]
• 63: Replication Features of the Splice Architecture [7]
• 68: Positive Acknowledgement Retransmission (PAR) Protocol [8]
• 69: Jackal Distributed Shared Memory Implementation of Java [9]
• 70: Distributed Data Space Architectures Described in Space Calculus [10]
• 71: Parallel Programs Developed using JavaSpaces (TM) [11]
• 81: Formal Verification of a Fair Payment Protocol [12]
• 87: Verification of a Fair Non-Repudiation Protocol [13]
• 89: Verifying Fault-Tolerant Erlang Programs [14]
• 92: Formal Specification and Verification of a DRM Protocol [15]

A set of benchmark models that includes mCRL2 specifications is the BEEM collection.

If you know of any other showcase to be listed here or any other related information, please contact info@mcrl2.win.tue.nl