Verification Support for workflow Design with UML Activity Graphs

Eshuis, Rik and Wieringa, Roel (2002) Verification Support for workflow Design with UML Activity Graphs. In: 24th International Conference on Software Engineering, ICSE 2002, May 19-25, 2002, Orlando, FL, USA.

Preview

PDF
1206Kb

Abstract:	We describe a tool that supports verification of workflow models specified in UML activity graphs. The tool translates an activity graph into an input format for a model checker according to a semantics we published earlier. 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. The tool automatically translates such an error trace into an activity graph trace by highlighting a corresponding path in the activity graph. One of the problems that is dealt with is that model checkers require a finite state space whereas workflow models in general have an infinite state space. Another problem is that strong fairness is necessary to obtain realistic results. Only model checkers that use a special model checking algorithm for strong fairness are suitable for verifying workflow models. We analyse the structure of the state space. We illustrate our approach with some example verifications.
Item Type:	Conference or Workshop Item
Copyright:	©2002 Association for Computing Machinery
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Information Systems (IS)
Link to this item:	http://purl.utwente.nl/publications/38257
Official URL:	http://dx.doi.org/10.1145/581339.581362
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 209499