Abstract
| Original language | English |
|---|---|
| Pages (from-to) | 437-447 |
| Number of pages | 11 |
| Journal | IEEE transactions on software engineering |
| Volume | 30 |
| Issue number | 7 |
| DOIs | |
| Publication status | Published - Jul 2004 |
Fingerprint
Keywords
- METIS-222902
- EWI-10481
- SCS-Services
- IR-64187
Cite this
}
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 journal › Article › Academic › peer-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 -