The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.07 - July (2004 vol.30)
pp: 437-447
ABSTRACT
<p><b>Abstract</b>—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.</p>
INDEX TERMS
Analysis, tools, software/program verification, model checking, state diagrams, workflow management.
CITATION
Rik Eshuis, "Tool Support for Verifying UML Activity Diagrams", IEEE Transactions on Software Engineering, vol.30, no. 7, pp. 437-447, July 2004, doi:10.1109/TSE.2004.33
27 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool