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 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 |
Keywords
- METIS-222902
- EWI-10481
- SCS-Services
- IR-64187