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)
    91 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 -