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.
Description
Welcome to IEEE Xplore 2.0: Tool support for verifying UML activity diagrams
%0 Journal Article
%1 Eshuis2004
%A Eshuis, R.
%A Wieringa, R.
%B Software Engineering, IEEE Transactions on
%D 2004
%K LTL UML activity diagrams model-checker tool
%P 437- 447
%R 10.1109/TSE.2004.33
%T Tool support for verifying UML activity diagrams
%U http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=1318605&isnumber=29218&fromcon
%V 30
%X 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.
@article{Eshuis2004,
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.},
added-at = {2008-06-12T13:00:50.000+0200},
author = {Eshuis, R. and Wieringa, R.},
biburl = {https://www.bibsonomy.org/bibtex/21c364961b0a82684d9a8278844d4ddb2/ist_spl},
booktitle = {Software Engineering, IEEE Transactions on},
description = {Welcome to IEEE Xplore 2.0: Tool support for verifying UML activity diagrams},
doi = {10.1109/TSE.2004.33},
interhash = {bbd27863d175a893d4c2bd531345c08c},
intrahash = {1c364961b0a82684d9a8278844d4ddb2},
issn = {0098-5589},
keywords = {LTL UML activity diagrams model-checker tool},
note = {MR: vielleicht nur wegen der Behandlung von UML-Aktivitätsdiagrammen interessant.},
pages = {437- 447},
timestamp = {2008-06-12T13:00:50.000+0200},
title = {Tool support for verifying UML activity diagrams},
url = {http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=1318605&isnumber=29218&fromcon},
volume = 30,
year = 2004
}