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

    32 Citations (Scopus)
    107 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