Suitability of mCRL2 for concurrent system design: a 2x2 switch case study
| Autor: | Stappers, F.P.M., Reniers, M.A., Groote, J.F., Boer, de, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. |
|---|---|
| Přispěvatelé: | Formal System Analysis |
| Jazyk: | angličtina |
| Rok vydání: | 2010 |
| Předmět: | |
| Zdroj: | Formal Methods for Components and Objects ISBN: 9783642170706 FMCO Formal Methods for Components and Objects (FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers), 166-185 STARTPAGE=166;ENDPAGE=185;TITLE=Formal Methods for Components and Objects (FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers) |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-642-17071-3_9 |
| Popis: | 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 multiparty 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|