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 条

[1] Family-Based Model Checking with mCRL2
ter Beek, Maurice H.
de Vink, Erik P.
Willemse, Tim A. C.
[J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2017, 2017, 10202 : 387 - 405
[2] Model Checking Business Processes for Web Service Compositions in mCRL2
Sun, Meng
Li, Shaodong
Ou, Yufei
[J]. 2014 SIXTH INTERNATIONAL CONFERENCE ON INTELLIGENT HUMAN-MACHINE SYSTEMS AND CYBERNETICS (IHMSC), VOL 2, 2014, : 202 - 205
[3] 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
[4] Analysing AWN-Specifications Using mCRL2
van Glabbeek, Rob
Hofner, Peter
van der Wal, Djurre
[J]. INTEGRATED FORMAL METHODS, IFM 2018, 2018, 11023 : 398 - 418
[5] Family-Based Model Checking of SPL based on mCRL2
Ben Snaiba, Ziad
de Vink, Erik P.
Willemse, Tim A. C.
[J]. 21ST INTERNATIONAL SYSTEM & SOFTWARE PRODUCT LINE CONFERENCE (SPLC 2017), VOL 2, 2017, : 13 - 16
[6] Formal verification of OIL component specifications using mCRL2
Olav Bunte
Louis C. M. van Gool
Tim A. C. Willemse
[J]. International Journal on Software Tools for Technology Transfer, 2022, 24 : 441 - 472
[7] Formal Verification of an Industrial UML-like Model using mCRL2
Stramaglia, Anna
Keiren, Jeroen J. A.
[J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2022), 2022, 13487 : 86 - 102
[8] Formal Verification of OIL Component Specifications using mCRL2
Bunte, Olav
van Gool, Louis C. M.
Willemse, Tim A. C.
[J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2020, 2020, 12327 : 231 - 251
[9] Formal verification of OIL component specifications using mCRL2
Bunte, Olav
van Gool, Louis C. M.
Willemse, Tim A. C.
[J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (03) : 441 - 472
[10] Model checking for an executable subset of UML
Xie, F
Levin, V
Browne, JC
[J]. 16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 333 - 336

← 1 2 3 4 5 →