Symbolic model checking of UML activity diagrams

ABSTRACT

Two translations from activity diagrams to the input language of NuSMV, a symbolic model verifier, are presented. Both translations map an activity diagram into a finite state machine and are inspired by existing statechart semantics. The requirements-level translation defines state machines that can be efficiently verified, but are a bit unrealistic since they assume the perfect synchrony hypothesis. The implementation-level translation defines state machines that cannot be verified so efficiently, but that are more realistic since they do not use the perfect synchrony hypothesis. To justify the use of the requirements-level translation, we show that for a large class of activity diagrams and certain properties, both translations are equivalent: regardless of which translation is used, the outcome of model checking is the same. Moreover, for linear stuttering-closed properties, the implementation-level translation is equivalent to a slightly modified version of the requirements-level translation. We use the two translations to model check data integrity constraints for an activity diagram and a set of class diagrams that specify the data manipulated in the activities. Both translations have been implemented in two tools. We discuss our experiences in applying both translations to model check some large example activity diagrams.

REFERENCES

• 1: Alonso, G., Casati, F., Kuno, H., and Machiraju, V. 2004. Web Services: Concepts, Architectures and Applications. Springer.
• 2: Charles Andre , Frederic Boulanger , Alain Girault, Software Implementation of Synchronous Programs, Proceedings of the Second International Conference on Application of Concurrency to System Design, p.133, June 25-29, 2001
• 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: Bock, C. 1999. Unified behavior models. J. Object-Oriented Prog. 12, 5.
• 5: Barry W. Boehm, Software Engineering Economics, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 6: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 7: M. C. Browne , E. M. Clarke , O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science, v.59 n.1-2, p.115-131, July 1988 [doi>10.1016/0304-3975(88)90098-9]
• 8: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 9: Campbell, L., Cheng, B., McUmber, W., and Stirewalt, R. 2002. Automatically detecting and visualising errors in UML diagrams. Requirements Eng. J. 7, 264--287.
• 10: Caspers, A. 1998. Workflow management: Analyse, modellering en implementatie (in Dutch). M.S. thesis, Vrije Universiteit Amsterdam.
• 11: 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]
• 12: Alessandro Cimatti , Edmund M. Clarke , Enrico Giunchiglia , Fausto Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.359-364, July 27-31, 2002
• 13: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 14: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 15: Dehne, F., Wieringa, R., and van de Zandschulp, H. 2000. Toolkit for conceptual modeling (TCM)---user's guide and reference. Tech. Rep., University of Twente.
• 16: Jörg Desel , Javier Esparza, Free choice Petri nets, Cambridge University Press, New York, NY, 1995
• 17: E. Allen Emerson , Somesh Jha , Doron Peled, Combining Partial Order and Symmetry Reductions, Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.19-34, April 02-04, 1997
• 18: Hans-Erik Eriksson , Magnus Penker, Business Modeling With UML: Business Patterns at Work, John Wiley & Sons, Inc., New York, NY, 1998
• 19: Eshuis, R. 2002. Semantics and verification of UML activity diagrams for workflow modelling. Ph.D. thesis, Centre for Telematics and Information Technology, University of Twente. Available at http://www.ctit.utwente.nl/library/phd/eshuis.pdf.
• 20: Eshuis, R., Jansen, D., and Wieringa, R. 2002. Requirements-level semantics and model checking of object-oriented statecharts. Requirements Eng. J. 7, 243--263.
• 21: 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
• 22: 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
• 23: Rik Eshuis , Roel Wieringa, Verification support for workflow design with UML activity graphs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581362]
• 24: Eshuis, R. and Wieringa, R. 2003. Comparing Petri net and activity diagram variants for workflow modelling---a quest for reactive Petri nets. In Petri Net Technology for Communication Based Systems, H. Ehrig, W. Reisig, G. Rozenberg, and H. Weber, Eds. Lecture Notes in Computer Science 2472. Springer, 321--351.
• 25: Tool Support for Verifying UML Activity Diagrams, IEEE Transactions on Software Engineering, v.30 n.7, p.437-447, July 2004 [doi>10.1109/TSE.2004.33]
• 26: Paul Grefen , Barbara Pernici , Gabriel Sanchez, Database Support for Workflow Management: The Wide Project, Kluwer Academic Publishers, Norwell, MA, 1999
• 27: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 28: 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]
• 29: Jan Hendrik Hausmann , Reiko Heckel , Gabi Taentzer, Detection of conflicting functional requirements in a use case-driven approach: a static analysis technique based on graph transformation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581355]
• 30: 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]
• 31: Paola Inverardi , Henry Muccini , Patrizio Pelliccione, Automated Check of Architectural Models Consistency Using SPIN, Proceedings of the 16th IEEE international conference on Automated software engineering, p.346, November 26-29, 2001
• 32: 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
• 33: Lamport, L. 1983. What good is temporal logic? In Proceedings of the IFIP Congress on Information Processing, R.E.A. Mason, Ed. North-Holland, 657--667.
• 34: Latella, D., Majzik, I., and Massink, M. 1999. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing 11, 6, 637--664.
• 35: Lilius, J. and Paltor, I. P. 1999. Formalizing UML state machines for model checking. In Proceedings of ≪UML≫ 2001, R. France and B. Rumpe, Eds. Lecture Notes in Computer Science 1723. Springer, 430--445.
• 36: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 37: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 38: MIT. MIT process handbook. http://ccs.mit.edu/ph.
• 39: Murata, T. 1989. Petri nets: Properties, analysis, and applications. In Proceedings of the IEEE 77, 4, 541--580.
• 40: No Magic, Inc. MagicDraw. http://www.magicdraw.com.
• 41: Barbara Paech, On the Role of Activity Diagrams in UML - A User Task Centered Development Process for UML, Selected papers from the First International Workshop on The Unified Modeling Language «UML»'98: Beyond the Notation, p.267-277, June 03-04, 1998
• 42: Doron Peled, All from One, One for All: on Model Checking Using Representatives, Proceedings of the 5th International Conference on Computer Aided Verification, p.409-423, June 28-July 01, 1993
• 43: Doron Peled, On projective and separable properties, Theoretical Computer Science, v.186 n.1-2, p.135-156, Oct. 30, 1997 [doi>10.1016/S0304-3975(96)00225-3]
• 44: 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
• 45: RosettaNet consortium. RosettaNet. http://www.rosettanet.org.
• 46: Schäfer, T., Knapp, A., and Merz, S. 2001. Model checking UML state machines and collaborations. In Proceedings of the Workshop on Software Model Checking, S. Stoller and W. Visser, Eds. Electronic Notes in Theoretical Computer Science 55, 3.
• 47: Bran Selic, Physical Programming: Beyond Mere Logic, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.1, April 02-06, 2001
• 48: TCM 2005. Toolkit for conceptual modeling (TCM). Available at http://www.cs.utwente.nl/~tcm.
• 49: UML Revision Taskforce. 2003a. OMG UML Specification v. 1.5. Object Management Group. OMG Document Number formal/2003-03-01. Available at http://www.omg.org.
• 50: UML Revision Taskforce. 2003b. UML 2.0 Superstructure Specification. Object Management Group. OMG Document Number ptc/03-07-06. Available at http://www.omg.org.
• 51: UN/CEFACT and OASIS. ebXML. http://www.ebxml.org.
• 52: Jin Yang , Aloysius K. Mok , Farn Wang, Symbolic model checking for event-driven real-time systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.386-412, March 1997 [doi>10.1145/244795.244803]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: State diagrams

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Model checking

General Terms:
Verification

Keywords:
Model checking, Unified Modeling Language, activity diagrams