Towards Model Checking Executable UML Specifications in mCRL2

Helle Hvid Hansen, J. Ketema, Bas Luttik, MohammadReza Mousavi, Jan Cornelis van de Pol

Research output: Contribution to journalArticleAcademicpeer-review

29 Citations (Scopus)
85 Downloads (Pure)

Abstract

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.
Original languageUndefined
Article number10.1007/s11334-009-0116-1
Pages (from-to)83-90
Number of pages8
JournalInnovations in systems and software engineering
Volume6
Issue number1-2
DOIs
Publication statusPublished - Mar 2010

Keywords

  • EWI-17667
  • IR-70349
  • METIS-277400
  • Software verification and validation - Specification languages - Model checking - Executable UML - Process algebra

Cite this

Hansen, Helle Hvid ; Ketema, J. ; Luttik, Bas ; Mousavi, MohammadReza ; van de Pol, Jan Cornelis. / Towards Model Checking Executable UML Specifications in mCRL2. In: Innovations in systems and software engineering. 2010 ; Vol. 6, No. 1-2. pp. 83-90.
@article{9ae09b4f70014d27af65a360fa2f1708,
title = "Towards Model Checking Executable UML Specifications in mCRL2",
abstract = "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.",
keywords = "EWI-17667, IR-70349, METIS-277400, Software verification and validation - Specification languages - Model checking - Executable UML - Process algebra",
author = "Hansen, {Helle Hvid} and J. Ketema and Bas Luttik and MohammadReza Mousavi and {van de Pol}, {Jan Cornelis}",
note = "Open Access",
year = "2010",
month = "3",
doi = "10.1007/s11334-009-0116-1",
language = "Undefined",
volume = "6",
pages = "83--90",
journal = "Innovations in systems and software engineering",
issn = "1614-5046",
publisher = "Springer",
number = "1-2",

}

Hansen, HH, Ketema, J, Luttik, B, Mousavi, M & van de Pol, JC 2010, 'Towards Model Checking Executable UML Specifications in mCRL2' Innovations in systems and software engineering, vol. 6, no. 1-2, 10.1007/s11334-009-0116-1, pp. 83-90. https://doi.org/10.1007/s11334-009-0116-1

Towards Model Checking Executable UML Specifications in mCRL2. / Hansen, Helle Hvid; Ketema, J.; Luttik, Bas; Mousavi, MohammadReza; van de Pol, Jan Cornelis.

In: Innovations in systems and software engineering, Vol. 6, No. 1-2, 10.1007/s11334-009-0116-1, 03.2010, p. 83-90.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Towards Model Checking Executable UML Specifications in mCRL2

AU - Hansen, Helle Hvid

AU - Ketema, J.

AU - Luttik, Bas

AU - Mousavi, MohammadReza

AU - van de Pol, Jan Cornelis

N1 - Open Access

PY - 2010/3

Y1 - 2010/3

N2 - 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.

AB - 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.

KW - EWI-17667

KW - IR-70349

KW - METIS-277400

KW - Software verification and validation - Specification languages - Model checking - Executable UML - Process algebra

U2 - 10.1007/s11334-009-0116-1

DO - 10.1007/s11334-009-0116-1

M3 - Article

VL - 6

SP - 83

EP - 90

JO - Innovations in systems and software engineering

JF - Innovations in systems and software engineering

SN - 1614-5046

IS - 1-2

M1 - 10.1007/s11334-009-0116-1

ER -