Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Suitability of mCRL2 for Concurrent-System Design: A 2 × 2 Switch Case Study
verfasst von : Frank P. M. Stappers, Michel A. Reniers, Jan Friso Groote
Erschienen in: Formal Methods for Components and Objects
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.