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

    12 Citations (Scopus)
    1 Downloads (Pure)


    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
    Number of pages26
    ISBN (Print)978-3-642-25270-9
    Publication statusPublished - Nov 2011

    Publication series

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


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

    Cite this