Showcases

From MCRL2

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

• Automated parking garage
• AIA ITP load-balancer
• Distributed system for lifting trucks
• IEEE 1394 link layer
• Patient support platform
• Automatic document feeder
• Generic driving actuator
• Pacemaker

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 showcases@mcrl2.org