Issue No. 07 - July (2004 vol. 30)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2004.33
<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>
Analysis, tools, software/program verification, model checking, state diagrams, workflow management.
R. Wieringa and R. Eshuis, "Tool Support for Verifying UML Activity Diagrams," in IEEE Transactions on Software Engineering, vol. 30, no. , pp. 437-447, 2004.