Tool support for verifying UML activity diagrams

H. Eshuis, Roelf J. Wieringa

    Research output: Contribution to journalArticleAcademicpeer-review

    105 Citations (Scopus)

    Abstract

    We describe a tool that supports verification of workflow models specified in UML activity diagrams. The tool translates an activity diagram into an input format for a model checker according to a mathematical semantics. With the model checker, arbitrary propositional requirements can be checked against the input model. If a requirement fails to hold, an error trace is returned by the model checker, which our tool presents by highlighting a corresponding path in the activity diagram. We summarize our formal semantics, discuss the techniques used to reduce an infinite state space to a finite one, and motivate the need for strong fairness constraints to obtain realistic results. We define requirement-preserving rules for state space reduction. Finally, we illustrate the whole approach with a few example verifications.
    Original languageEnglish
    Pages (from-to)437-447
    Number of pages11
    JournalIEEE transactions on software engineering
    Volume30
    Issue number7
    DOIs
    Publication statusPublished - Jul 2004

    Keywords

    • METIS-222902
    • EWI-10481
    • SCS-Services
    • IR-64187

    Fingerprint Dive into the research topics of 'Tool support for verifying UML activity diagrams'. Together they form a unique fingerprint.

  • Cite this