Tool support for verifying UML activity diagrams

Share/Save/Bookmark

Eshuis, Rik and Wieringa, Roel (2004) Tool support for verifying UML activity diagrams. IEEE Transactions on Software Engineering, 30 (7). pp. 437-447. ISSN 0098-5589

open access
[img] PDF
769kB
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.
Item Type:Article
Copyright:© 2004 IEEE
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/64187
Official URL:http://dx.doi.org/10.1109/TSE.2004.33
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 222902