Information Technology Reference
In-Depth Information
Suitability of mCRL2 for Concurrent-System
Design:
×
A2
2 Switch Case Study
Frank P.M. Stappers, Michel A. Reniers, and Jan Friso Groote
Department of Computer Science, Eindhoven University of Technology,
P.O. Box 513, NL-5600MB Eindhoven, The Netherlands
Abstract.
Specifying concurrent systems can be done using a variety
of languages. These languages have different features and therefore are
not necessarily equally suitable for capturing concepts from reality with
respect to both expressivity and ease-of-use.
This paper addresses these aspects for the specification language
mCRL2 by considering the 2
×
2 Switch case study. This case study has
been used before to compare other specification languages, more specif-
ically TLA+, Bluespec, Statecharts and ACP. The case study primarily
focuses on two important features, namely multi-party communication
and priority of certain actions over other actions. We show that mCRL2 is
appropriate for the specification of these features, especially multi-party
communication. Moreover, we express some of the requirements of the
original case study in terms of modal
µ
-calculus formulae and establish
that these are indeed satisfied by the model.
1
Introduction
In today's world, there are many different ways to specify system's behavior. At
first, many specification languages seem suitable for describing system behaviour,
as they are applied to case studies and toy examples that are specially tailored to
assess certain features of a language. Unfortunately, when actual systems need to
be specified, it often turns out that a language cannot express a certain amount of
behavior, as the language is too generic or too limited, and therefore not vigorous
enough to express complex behavioral patterns. This way, designers are required
to deviate from the system's behaviour or they have to apply abstractions such
that inexpressible behavior becomes irrelevant.
When designs are finished, it is dicult to ensure that a system meets the
requirements that were agreed upon in advance. In many cases human reasoning
is applied to validate that a system meets these requirements. However, a proof
or guarantee cannot be given. Especially for mission critical systems, but also for
concurrent systems, this might yield to undesired behaviour, which can result
into catastrophic disasters.
Selecting a suitable language for system design is a dicult task. To guide
designers, the authors of [6] have recently compared the specification languages
TLA+, Bluespec, Statecharts, and ACP for a particular case study. The authors
of [6] compare these languages with respect to the following three criteria:
