Automated Verification of Executable UML Models

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    11 Citations (Scopus)
    1 Downloads (Pure)

    Abstract

    We present a fully automated approach to verifying safety properties of Executable UML models (xUML). Our tool chain consists of a model transformation program which translates xUML models to the process algebra mCRL2, followed by symbolic model checking using LTSmin. If a safety violation is found, an error trace is visualised as a UML sequence diagram. As a novel feature, our approach allows safety properties to be specied as UML state machines.
    Original languageUndefined
    Title of host publicationProceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers
    Place of PublicationBerlin
    PublisherSpringer
    Pages225-250
    Number of pages26
    ISBN (Print)978-3-642-25270-9
    DOIs
    Publication statusPublished - Nov 2011

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume6957
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • METIS-284928
    • EWI-21051
    • IR-79011

    Cite this

    Hansen, H. H., Ketema, J., Luttik, B., Mousavi, M., van de Pol, J. C., & Marchi dos Santos, O. (2011). Automated Verification of Executable UML Models. In Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers (pp. 225-250). (Lecture Notes in Computer Science; Vol. 6957). Berlin: Springer. https://doi.org/10.1007/978-3-642-25271-6_12
    Hansen, Helle Hvid ; Ketema, J. ; Luttik, Bas ; Mousavi, MohammadReza ; van de Pol, Jan Cornelis ; Marchi dos Santos, Oscar. / Automated Verification of Executable UML Models. Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers. Berlin : Springer, 2011. pp. 225-250 (Lecture Notes in Computer Science).
    @inproceedings{45fe3b8a5eba462f8fd8228fe828a7c7,
    title = "Automated Verification of Executable UML Models",
    abstract = "We present a fully automated approach to verifying safety properties of Executable UML models (xUML). Our tool chain consists of a model transformation program which translates xUML models to the process algebra mCRL2, followed by symbolic model checking using LTSmin. If a safety violation is found, an error trace is visualised as a UML sequence diagram. As a novel feature, our approach allows safety properties to be specied as UML state machines.",
    keywords = "METIS-284928, EWI-21051, IR-79011",
    author = "Hansen, {Helle Hvid} and J. Ketema and Bas Luttik and MohammadReza Mousavi and {van de Pol}, {Jan Cornelis} and {Marchi dos Santos}, Oscar",
    note = "eemcs-eprint-21051",
    year = "2011",
    month = "11",
    doi = "10.1007/978-3-642-25271-6_12",
    language = "Undefined",
    isbn = "978-3-642-25270-9",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "225--250",
    booktitle = "Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers",

    }

    Hansen, HH, Ketema, J, Luttik, B, Mousavi, M, van de Pol, JC & Marchi dos Santos, O 2011, Automated Verification of Executable UML Models. in Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers. Lecture Notes in Computer Science, vol. 6957, Springer, Berlin, pp. 225-250. https://doi.org/10.1007/978-3-642-25271-6_12

    Automated Verification of Executable UML Models. / Hansen, Helle Hvid; Ketema, J.; Luttik, Bas; Mousavi, MohammadReza; van de Pol, Jan Cornelis; Marchi dos Santos, Oscar.

    Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers. Berlin : Springer, 2011. p. 225-250 (Lecture Notes in Computer Science; Vol. 6957).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Automated Verification of Executable UML Models

    AU - Hansen, Helle Hvid

    AU - Ketema, J.

    AU - Luttik, Bas

    AU - Mousavi, MohammadReza

    AU - van de Pol, Jan Cornelis

    AU - Marchi dos Santos, Oscar

    N1 - eemcs-eprint-21051

    PY - 2011/11

    Y1 - 2011/11

    N2 - We present a fully automated approach to verifying safety properties of Executable UML models (xUML). Our tool chain consists of a model transformation program which translates xUML models to the process algebra mCRL2, followed by symbolic model checking using LTSmin. If a safety violation is found, an error trace is visualised as a UML sequence diagram. As a novel feature, our approach allows safety properties to be specied as UML state machines.

    AB - We present a fully automated approach to verifying safety properties of Executable UML models (xUML). Our tool chain consists of a model transformation program which translates xUML models to the process algebra mCRL2, followed by symbolic model checking using LTSmin. If a safety violation is found, an error trace is visualised as a UML sequence diagram. As a novel feature, our approach allows safety properties to be specied as UML state machines.

    KW - METIS-284928

    KW - EWI-21051

    KW - IR-79011

    U2 - 10.1007/978-3-642-25271-6_12

    DO - 10.1007/978-3-642-25271-6_12

    M3 - Conference contribution

    SN - 978-3-642-25270-9

    T3 - Lecture Notes in Computer Science

    SP - 225

    EP - 250

    BT - Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers

    PB - Springer

    CY - Berlin

    ER -

    Hansen HH, Ketema J, Luttik B, Mousavi M, van de Pol JC, Marchi dos Santos O. Automated Verification of Executable UML Models. In Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers. Berlin: Springer. 2011. p. 225-250. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-25271-6_12