Towards model checking executable UML specifications in mCRL2

被引：24
|
作者：
Hansen, Helle Hvid [1 ]
Ketema, Jeroen [2 ]
Luttik, Bas [1 ]
Mousavi, MohammadReza [1 ]
van de Pol, Jaco [2 ]
机构：
[1] Eindhoven Univ Technol, Eindhoven, Netherlands
[2] Univ Twente, Enschede, Netherlands
来源：
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING | 2010年 / 6卷 / 1-2期
关键词：
Software verification and validation; Specification languages; Model checking; Executable UML; Process algebra;
D O I：
10.1007/s11334-009-0116-1
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We describe a translation of a subset of executable UML (xUML) into the process algebraic specification language mCRL2. This subset includes class diagrams with class generalisations, and state machines with signal and change events. The choice of these xUML constructs is dictated by their use in the modelling of railway interlocking systems. The long-term goal is to verify safety properties of interlockings modelled in xUML using the mCRL2 and LTSmin toolsets. Initial verification of an interlocking toy example demonstrates that the safety properties of model instances depend crucially on the run-to-completion assumptions.
引用
收藏
页码：83 / 90
页数：8
相关论文
共 50 条
  • [21] 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
  • [22] Model checking UML specifications of real time software
    Del Bianco, V
    Lavazza, L
    Mauri, M
    [J]. EIGHTH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2002, : 203 - 212
  • [23] Formalising the Dezyne Modelling Language in mCRL2
    van Beusekom, Rutger
    Groote, Jan Friso
    Hoogendijk, Paul
    Howe, Robert
    Wesselink, Wieger
    Wieringa, Rob
    Willemse, Tim A. C.
    [J]. CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION (FMICS-AVOCS 2017), 2017, 10471 : 217 - 233
  • [24] An Overview of the mCRL2 Modelling and Verification Toolset
    Groote, Jan Friso
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (338): : 1 - 1
  • [25] Formal Modelling and Verification of an Interlocking Using mCRL2
    Bouwman, Mark
    Janssen, Bob
    Luttik, Bas
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2019, 2019, 11687 : 22 - 39
  • [26] An Overview of the mCRL2 Toolset and Its Recent Advances
    Cranen, Sjoerd
    Groote, Jan Friso
    Keiren, Jeroen J. A.
    Stappers, Frank P. M.
    de Vink, Erik P.
    Wesselink, Wieger
    Willemse, Tim A. C.
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 199 - 213
  • [27] Towards Executable Specifications for Microservices
    Quenum, Jose G.
    Aknine, Samir
    [J]. 2018 IEEE INTERNATIONAL CONFERENCE ON SERVICES COMPUTING (IEEE SCC 2018), 2018, : 41 - 48
  • [28] Modelling and Analysing a Mechanical Lung Ventilator in mCRL2
    van Dortmont, Danny
    Keiren, Jeroen J. A.
    Willemse, Tim A. C.
    [J]. RIGOROUS STATE-BASED METHODS, ABZ 2024, 2024, 14759 : 341 - 359
  • [29] Modelling the Raft Distributed Consensus Protocol in mCRL2
    Bora, Parth
    Minh, Pham Duc
    Willemse, Tim A. C.
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2024, (399): : 7 - 20
  • [30] Specification and analysis of hardware designs using mCRL2
    Man, K. L.
    van der Wulp, J.
    [J]. 2008 CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1-4, 2008, : 202 - +
12345