Date and Time: Thursday, 17 June 2010, 15:45 - 16:45

Location: HG 6.96

Speaker: Michel Reniers (OAS)

Title: Suitability of mCRL2 for Concurrent-System Design – A 2 x 2 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 x 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 better suited than those other languages for the specification of the case study. Moreover, we express some of the requirements of the original case study in terms of modal mu-calculus formulae and establish that these are indeed satisfied by the model.

This is joint work with Frank Stappers and Jan Friso Groote