hh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Towards model checking executable UML specifications in mCRL2
Eindhoven University of Technology, Eindhoven, Netherlands.
University of Twente, Enschede, Netherlands.
Eindhoven University of Technology, Eindhoven, Netherlands.
Eindhoven University of Technology, Eindhoven, Netherlands.ORCID iD: 0000-0002-4869-6794
Show others and affiliations
2010 (English)In: Innovations in Systems and Software Engineering, ISSN 1614-5046, Vol. 6, no 1, 83-90 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
London: Springer London, 2010. Vol. 6, no 1, 83-90 p.
Keyword [en]
Executable UML, Model checking, Process algebra, Software verification and validation, Specification languages
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:hh:diva-20519DOI: 10.1007/s11334-009-0116-1Scopus ID: 2-s2.0-77949321817OAI: oai:DiVA.org:hh-20519DiVA: diva2:584486
Available from: 2013-01-09 Created: 2013-01-08 Last updated: 2014-11-11Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Mousavi, Mohammad Reza
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 107 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf