Towards Model Checking Executable UML Specifications in mCRL2

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

doi:10.1007/s11334-009-0116-1

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 journal › Article › Academic › peer-review

36 Citations (Scopus)

151 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 language	Undefined
Article number	10.1007/s11334-009-0116-1
Pages (from-to)	83-90
Number of pages	8
Journal	Innovations in systems and software engineering
Volume	6
Issue number	1-2
DOIs	https://doi.org/10.1007/s11334-009-0116-1
Publication status	Published - Mar 2010

Keywords

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

Access to Document

10.1007/s11334-009-0116-1

http://eprints.eemcs.utwente.nl/secure2/17667/02/ketema-fulltext.pdf

Cite this

@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 = mar,

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",

}

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 -