This Article 
 Bibliographic References 
 Add to: 
Tool Support for Verifying UML Activity Diagrams
July 2004 (vol. 30 no. 7)
pp. 437-447

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.

[1] W.M.P. van der Aalst, P.J.N. de Crom, R.R.H.M.J. Goverde, K.M. van Hee, W.J. Hofman, H.A. Reijers, and R.A. van der Toorn, Exspect 6.4: An Executable Specification Tool for Hierarchical Colored Petri Nets Proc. 21st Int'l Conf. Applications and Theory of Petri Nets, M. Nielsen and D. Simpson, eds., 2000.
[2] E. Asarin, O. Maler, and A. Pnueli, On Discretization of Delays in Timed Automata and Digital Circuits Proc. Int'l Conf. Concurrency Theory (CONCUR '98), R. de Simone and D. Sangiorgi, eds., 1998.
[3] G. Berry and G. Gonthier, The EsterelSynchronous Programming Language: Design, Semantics, Implementation Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992
[4] C. Bussler, Enterprise-Wide Workflow Management IEEE Concurrency, vol. 7, no. 3, pp. 32-43, 1999.
[5] W. Chan, R.J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J.D. Reese, "Model Checking Large Software Specifications," IEEE Trans. Software Eng., vol. 24, no. 7, July 1998.
[6] W. Chan, R.J. Anderson, P. Beame, D.H. Jones, D. Notkin, and W.E. Warner, Optimizing Symbolic Model Checking for Statecharts IEEE Trans. Software Eng., vol. 27, no. 2, pp. 170-190, Feb. 2001.
[7] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, NuSMV: A New Symbolic Model Checker Int'l J. Software Tools for Technology Transfer, vol. 2, no. 4, pp. 410-425, 2000.
[8] E.M. Clarke, M. Fujita, S.P. Rajan, T. Reps, S. Shankar, and T. Teitelbaum, Program Slicing for VHDL Int'l J. Software Tools for Technology Transfer, vol. 4, no. 1, pp. 125-137, 2002.
[9] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 1999.
[10] W. Damm, B. Josko, H. Hungar, and A. Pnueli, A Compositional Real-Time Semantics of STATEMATE Designs Proc. Int'l Symp. Compositionality, W.-P. de Roever, H. Langmaack, and A. Pnueli, eds., 1998.
[11] F. Dehne, R. Wieringa, and H. van de Zandschulp, Toolkit for Conceptual Modeling (TCM) User's Guide and Reference technical report, Univ. of Twente, 2000, http://www.cs.utwente. nltcm.
[12] R. Eshuis, Semantics and Verification of UML Activity Diagrams for Workflow Modelling PhD thesis, Centre for Telematics and Information Technology, Univ. of Twente, 2002, http://www. .
[13] R. Eshuis and R. Wieringa, A Real-Time Execution Semantics for UML Activity Diagrams Proc. Conf. Fundamental Approaches to Software Eng. (FASE 2001), H. Hussmann, ed., 2001.
[14] R. Eshuis and R. Wieringa, An Execution Algorithm for UML Activity Graphs Proc. Fourth Int'l Conf. Unified Modeling Language (<<UML>>), M. Gogolla and C. Kobryn, eds., 2001.
[15] R. Eshuis and R. Wieringa, Verification Support for Workflow Design with UML Activity Graphs Proc. Int'l Conf. Software Eng. (ICSE 2002), pp. 166-176, 2002.
[16] R. Eshuis and R. Wieringa, Comparing Petri Net and Activity Diagram Variants for Workflow Modelling A Quest for Reactive Petri Nets Petri Net Technology for Comm. Based Systems, H. Ehrig, W. Reisig, G. Rozenberg, and H. Weber, eds., 2003.
[17] J. Esparza, Decidability of Model Checking for Infinite-State Concurrent Systems Acta Informatica, vol. 34, no. 2, pp. 85-107, 1997.
[18] R. Goldblatt, Logics of Time and Computation, second ed. Stanford Univ., 1992.
[19] P. Grefen, K. Aberer, Y. Hoffner, and H. Ludwig, Crossflow: Cross-Organizational Workflow Management in Dynamic Virtual Enterprises Int'l J. Computer Systems Science&Eng., vol. 15, no. 5, pp. 277-290, 2000.
[20] D. Harel and A. Naamad, The STATEMATE Semantics of Statecharts ACM Trans. Software Eng. and Methodology, vol. 5, no. 4, pp. 293-333, 1996.
[21] D. Harel and A. Pnueli, On the Development of Reactive Systems Logics and Models of Concurrent Systems, K.R. Apt, ed., 1985.
[22] D. Harel and M. Politi, Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, 1998.
[23] J. Hatcliff, M.B. Dwyer, and H. Zheng, Slicing Software for Model Construction Higher-Order and Symbolic Computation, vol. 13, no. 4, pp. 315-353, 2000.
[24] T.A. Henzinger, Z. Manna, and A. Pnueli, What Good Are Digital Clocks? Proc. Int'l Colloquium Automata, Languages, and Programming (ICALP '92), W. Kuich, ed., 1992.
[25] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[26] W. Janssen, R. Mateescu, S. Mauw, and J. Springintveld, Verifying Business Processes Using Spin Proc. Int'l Spin Workshop, E. Najm, A. Serhrouchni, and G. Holzmann, eds., 1998.
[27] C. Karamanolis, D. Giannakopoulou, J. Magee, and S. Wheater, Model Checking of Workflow Schemas Proc. Int'l Conf. Enterprise Distributed Object Computing (EDOC 2000), pp. 170-181, 2000.
[28] R.M. Karp and R.E. Miller, Parallel Program Schemata J. Computer and System Sciences, vol. 3, pp. 147-195, 1969.
[29] W.D. Kelton, R.P. Sadowski, and D.A. Sadowski, Simulation with Arena. McGraw-Hill, 1998.
[30] Y. Kesten, Z. Manna, and A. Pnueli, Verification of Clocked and Hybrid Systems Acta Informatica, vol. 36, no. 11, pp. 837-912, 2000.
[31] Y. Kesten, A. Pnueli, and L. Raviv, Algorithmic Verification of Linear Temporal Logic Specifications Proc. Int'l Colloquium Automata, Languages, and Programming (ICALP '98), K.G. Larsen, S. Skyum, and G. Winskel, eds., 1998.
[32] D. Latella, I. Majzik, and M. Massink, Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-Checker Formal Aspects of Computing, vol. 11, no. 6, pp. 637-664, 1999.
[33] J. Lilius and I.P. Paltor, vUML: A Tool for Verifying UML Models Proc. 14th IEEE Int'l Conf. Automated Software Eng., 1999.
[34] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer, 1992.
[35] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[36] P. Muth, D. Wodtke, J. Weissenfels, G. Weikum, and A. Kotz-Dittrich, Enterprise-Wide Workflow Management Based on State and Activity Charts Workflow Management Systems and Interoperability, A. Dogac, L. Kalinichenko, T.Özsu, and A. Sheth, eds., 1998.
[37] A. Pnueli and E. Shahar, A Platform Combining Deductive with Algorithmic Verification Proc. Int'l Conf. Computer Aided Verification (CAV '96), R. Alur and T.A. Henzinger, eds., 1996.
[38] P. Spruit, R. Wieringa, and J.J. Meyer, Regular Database Update Logics Theoretical Computer Science, vol. 254, nos. 1-2, pp. 591-661, 2001.
[39] UML Revision Taskforce, OMG UML Specification v.1.5 OMG Document Number formal/2003-03-01, Object Management Group, 2003, http:/
[40] F. Tip, A Survey of Program Slicing Techniques J. Programming Languages, vol. 3, pp. 121-189, 1995.
[41] H.M.W. Verbeek, T. Basten, and W.M.P. van der Aalst, Diagnosing Workflow Processes Using Woflan The Computer J., vol. 44, no. 4, pp. 246-279, 2001.
[42] R.J. Wieringa, Design Methods for Reactive Systems. Morgan Kaufmann, 2003.
[43] Workflow Management Coalition, Workflow Management Coalition Specification Terminology&Glossary WFMC document WFMC-TC-1011, 1999, available athttp:/

Index Terms:
Analysis, tools, software/program verification, model checking, state diagrams, workflow management.
Rik Eshuis, Roel Wieringa, "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
Usage of this product signifies your acceptance of the Terms of Use.