@inproceedings{82156df3b71142dd8fb9a36aeab0ebc6,
title = "Suitability of mCRL2 for concurrent system design: a 2x2 switch case study",
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 specifically 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.",
author = "F.P.M. Stappers and M.A. Reniers and J.F. Groote",
year = "2010",
doi = "10.1007/978-3-642-17071-3_9",
language = "English",
isbn = "978-3-642-17070-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "166--185",
editor = "{Boer, de}, F.S. and M.M. Bonsangue and S. Hallerstede and M. Leuschel",
booktitle = "Formal Methods for Components and Objects (FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers)",
address = "Germany",
}