Tool support for verifying UML activity diagrams

Research output: Contribution to journalArticleAcademicpeer-review

103 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

Fingerprint

Semantics

Keywords

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

Cite this

@article{53f672b731f748a2a7bd2d313a283349,
title = "Tool support for verifying UML activity diagrams",
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.",
keywords = "METIS-222902, EWI-10481, SCS-Services, IR-64187",
author = "H. Eshuis and Wieringa, {Roelf J.}",
year = "2004",
month = "7",
doi = "10.1109/TSE.2004.33",
language = "English",
volume = "30",
pages = "437--447",
journal = "IEEE transactions on software engineering",
issn = "0098-5589",
publisher = "IEEE",
number = "7",

}

Tool support for verifying UML activity diagrams. / Eshuis, H.; Wieringa, Roelf J.

In: IEEE transactions on software engineering, Vol. 30, No. 7, 07.2004, p. 437-447.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Tool support for verifying UML activity diagrams

AU - Eshuis, H.

AU - Wieringa, Roelf J.

PY - 2004/7

Y1 - 2004/7

N2 - 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.

AB - 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.

KW - METIS-222902

KW - EWI-10481

KW - SCS-Services

KW - IR-64187

U2 - 10.1109/TSE.2004.33

DO - 10.1109/TSE.2004.33

M3 - Article

VL - 30

SP - 437

EP - 447

JO - IEEE transactions on software engineering

JF - IEEE transactions on software engineering

SN - 0098-5589

IS - 7

ER -