From mu CRL to mCRL2

被引:10
|
作者
Groote, Jan Friso [1 ]
Mathijssen, Aad [1 ]
van Weerdenburg, Muck [1 ]
Usenko, Yaroslav [1 ]
机构
[1] Eindhoven Univ Technol, Dept Math & Comp Sci, POB 513, NL-5600 MB Eindhoven, Netherlands
关键词
mCRL2; process algebra; data types; behavioural analysis;
D O I
10.1016/j.entcs.2005.12.101
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We sketch the language mCRL2, the successor of mu CRL, which is a process algebra with data, devised in 1990 to model and study the behaviour of interacting programs and systems. The language is improved in several respects guided by the experience obtained from numerous applications where realistic systems have been modelled and analysed. Just as with mu CRL, the leading principle is to provide a minimal set of primitives that allow effective specifications, that conform to standard mathematics and that allow standard mathematical manipulations and proof methodologies. In the first place the equational abstract datatypes have been enhanced with higher-order constructs and standard data types, ranging from booleans, numbers and lists to sets, bags and higher-order function types. In the second place multi-actions have been introduced to allow a seamless integration with Petri nets. In the last place communication is made local to enable compositionality.
引用
收藏
页码:191 / 196
页数:6
相关论文
共 50 条
  • [1] Formalising the Industrial Language SMMT in mCRL2
    van Laarhoven, Jordi E. P. M.
    Bunte, Olav
    van Gool, Louis C. M.
    Willemse, Tim A. C.
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2024, 2024, 14952 : 63 - 79
  • [2] Sarir: A Rebeca to mCRL2 translator
    Hojjat, H.
    Siriani, M.
    Mousavi, M. R.
    Groote, J. F.
    [J]. SEVENTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2007, : 216 - +
  • [3] Modelling and Analysing Software in mCRL2
    Groote, Jan Friso
    Keiren, Jeroen J. A.
    Luttik, Bas
    de Vink, Erik P.
    Willemse, Tim A. C.
    [J]. FORMAL ASPECTS OF COMPONENT SOFTWARE, FACS 2019, 2020, 12018 : 25 - 48
  • [4] Experiences in developing the mCRL2 toolset
    Groote, J. F.
    Keiren, J. J. A.
    Stappers, F. P. M.
    Wesselink, J. W.
    Willemse, T. A. C.
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 2011, 41 (02): : 143 - 153
  • [5] ogfooding the formal semantics of mCRL2
    Stappers, F. P. M.
    Reniers, M. A.
    Weber, S.
    Groote, J. F.
    [J]. PROCEEDINGS OF THE 2012 IEEE 35TH SOFTWARE ENGINEERING WORKSHOP (SEW 2012), 2012, : 90 - 99
  • [6] XACML2mCRL2: Automatic transformation of XACML policies into mCRL2 specifications
    Arshad, Hamed
    Horne, Ross
    Johansen, Christian
    Owe, Olaf
    Willemse, Tim A. C.
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2024, 232
  • [7] Tutorial: Designing Distributed Software in mCRL2
    Groote, Jan Friso
    Keiren, Jeroen J. A.
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2021, 2021, 12719 : 226 - 243
  • [8] A Formalisation of SysML State Machines in mCRL2
    Bouwman, Mark
    Luttik, Bas
    Van der Wal, Djurre
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2021, 2021, 12719 : 42 - 59
  • [9] Verification of networks of timed automata using mCRL2
    Groote, Jan Friso
    Reniers, Michel A.
    Usenko, Yaroslav S.
    [J]. 2008 IEEE INTERNATIONAL SYMPOSIUM ON PARALLEL & DISTRIBUTED PROCESSING, VOLS 1-8, 2008, : 3782 - 3789
  • [10] An Overview of the mCRL2 Modelling and Verification Toolset
    Groote, Jan Friso
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (338): : 1 - 1