Verification support for workflow design with UML activity graphs

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 high-lighting 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.

REFERENCES

• 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. In M. Nielsen and D. Simpson, editors, Proc. 21st Int. Conf. on Applications and Theory of Petri Nets, LNCS 1825, 2000.
• 2: Wil M. P. van der Aalst , Alistair P. Barros , Arthur H. M. ter Hofstede , Bartek Kiepuszewski, Advanced Workflow Patterns, Proceedings of the 7th International Conference on Cooperative Information Systems, p.18-29, September 06-08, 2000
• 3: Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
• 4: Christoph Bussler, Enterprise-Wide Workflow Management, IEEE Concurrency, v.7 n.3, p.32-43, July 1999 [doi>10.1109/4434.788777]
• 5: William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998 [doi>10.1109/32.708566]
• 6: A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: A new symbolic model checker. Int. Journal on Software Tools for Technology Transfer, 2(4):410-425, 2000.
• 7: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 8: D. R. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, 1996.
• 9: F. Dehne, R. Wieringa, and H. van de Zandschulp. Toolkit for conceptual modeling (TCM) --- user's guide and reference. Technical report, University of Twente, 2000. http://www.cs.utwente.nl/~tcm.
• 10: R. Eshuis and R. Wieringa. A formal semantics for UML activity diagrams. Technical Report TR-CTIT-01-04, University of Twente, 2001.
• 11: Rik Eshuis , Roel Wieringa, A Real-Time Execution Semantics for UML Activity Diagrams, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.76-90, April 02-06, 2001
• 12: R. Eshuis and R. Wieringa. A comparison of Petri net and activity diagram variants. In Proc. 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems, 2001.
• 13: Rik Eshuis , Roel Wieringa, An Execution Algorithm for UML Activity Graphs, Proceedings of the 4th International Conference on The Unified Modeling Language, Modeling Languages, Concepts, and Tools, p.47-61, October 01-05, 2001
• 14: J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34(2):85-107, 1997.
• 15: Robert Goldblatt, Logics of time and computation, Center for the Study of Language and Information, Stanford, CA, 1987
• 16: A. Göllü, A. Puri, and P. Varaiya. Discretization of timed automata. In Proc. of the 33rd IEEE conferene on decision and control, pages 957-958, 1994.
• 17: Bernd Grahlmann, The PEP Tool, Proceedings of the 9th International Conference on Computer Aided Verification, p.440-443, June 22-25, 1997
• 18: P. Grefen, K. Aberer, Y. Hoffner, and H. Ludwig. Crossflow: Cross-organizational workflow management in dynamic virtual enterprises. Int. Journal of Comp. Systems Science & Engineering, 15(5):277-290, 2000.
• 19: David Harel , Amnon Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.293-333, Oct. 1996 [doi>10.1145/235321.235322]
• 20: D. Harel , A. Pnueli, On the development of reactive systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 21: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 22: J. Helbig and P. Kelb. An OBDD-Representation of Statecharts. In Proc. of the European Design and Test Conf., pages 142-151. IEEE Comp. Soc. Press, 1994.
• 23: W. Janssen, R. Mateescu, S. Mauw, and J. Springintveld. Verifying business processes using Spin. In E. Najm, A. Serhrouchni, and G. Holzmann, editors, Proc. 4th Int. Spin workshop, 1998.
• 24: R.M. Karp and R.E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3:147-195, 1969.
• 25: David W. Kelton , Randall P. Sadowski , Deborah A. Sadowski, Simulation with Arena, McGraw-Hill, Inc., New York, NY, 1997
• 26: Yonit Kesten , Amir Pnueli , Li-on Raviv, Algorithmic Verification of Linear Temporal Logic Specifications, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.1-16, July 13-17, 1998
• 27: 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, 11(6):637-664, 1999.
• 28: Johan Lilius , Ivan Porres Paltor, vUML: A Tool for Verifying UML Models, Proceedings of the 14th IEEE international conference on Automated software engineering, p.255, October 12-15, 1999
• 29: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 30: E. Mikk. Semantics and Verification of Statecharts. PhD thesis, University of Kiel, 2000.
• 31: P. Muth, D. Wodtke, J. Weissenfels, G. Weikum, and A. Kotz-Dittrich. Enterprise-wide workflow management based on state and activity charts. In A. Dogac, L. Kalinichenko, T. Özsu, and A. Sheth, editors, NATO/ASI Workflow Management Systems and Interoperability. Springer, 1998.
• 32: Amir Pnueli , Elad Shahar, A Platform for Combining Deductive with Algorithmic Verification, Proceedings of the 8th International Conference on Computer Aided Verification, p.184-195, August 03, 1996
• 33: UML Revision Taskforce. OMG UML Specification v. 1.4. Object Management Group, 2001.
• 34: H.M.W. Verbeek, T. Basten, and W.M.P. van der Aalst. Diagnosing workflow processes using Woflan. The Computer Journal, 44(4):246-279, 2001.
• 35: R. J. Wieringa, Design Methods for Software Systems: YOURDON, Statemate and Uml, Science & Technology Books, 2002
• 36: Workflow Management Coalition. Workflow management coalition specification --- terminology & glossary (WFMC-TC-1011), 1999. www.wfmc.org.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: UML

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Graph algorithms

General Terms:
Algorithms, Design, Performance