Games for UML Software Design

  • Perdita Stevens
  • Jennifer Tenzer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2852)


In this paper we introduce the idea of using games as a driving metaphor for design tools which support designers working in UML. We use as our basis a long strand of work in verification and elsewhere. A key difference from that strand, however, is that we propose the incremental development of the rules of a game as part of the design process. We will argue that this approach may have two main advantages. First, it provides a natural means for tools to interactively help the designer to explore the consequences of design decisions. Second, by providing a smooth progression from informal exploration of decisions to full verification, it has the potential to lower the commitment cost of using formal verification. We discuss a simple example of a possible game development.


Model Check Class Diagram Object Constraint Language Winning Strategy Winning Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: Dynamic programs for omega-regular objectives. In: Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS), pp. 279–290. IEEE Computer Society Press, Los Alamitos (2001)CrossRefGoogle Scholar
  2. 2.
    Fraenkel, A.S.: Selected bibliography on combinatorial games and some related material. The Electronic Journal of Combinatorics, DS2 (2002), Available from
  3. 3.
    Grädel, E.: Model checking games. In: Proceedings of WOLLIC 2002. Electronic Notes in Theoretical Computer Science, vol. 67. Elsevier, Amsterdam (2002)Google Scholar
  4. 4.
    Harel, D.: From play-in scenarios to code: An achievable dream. IEEE Computer 34(1), 53–60 (2001)MathSciNetGoogle Scholar
  5. 5.
    Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Hodges, W.: Model theory. Encyclopedia of Mathematics, vol. 42. Cambridge University Press, Cambridge (1993)zbMATHCrossRefGoogle Scholar
  7. 7.
    Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open systems in reactive enfironments: control and synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 92–107. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  8. 8.
    Kupferman, O., Vardi, M.Y.: Synthesising distributed systems. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001). IEEE Computer Society, Los Alamitos (June 2001)Google Scholar
  9. 9.
    Madhusudan, P., Thiagarajan, P.S.: Branching time controllers for discrete event systems. Theoretical Computer Science 274(1-2), 117–149 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    OMG. Unified Modeling Language Specification version 1.4 (September 2001), OMG document formal/01-09-67 available from
  11. 11.
    Stevens, P.: Abstract interpretations of games. In: Proc. 2nd International Workshop on Verification, Model Checking and Abstract Interpretation, VMCAI 1998. Venezia TR, vol. CS98-12 (1998)Google Scholar
  12. 12.
    Stirling, C.: Model checking and other games. In: Notes for Mathfit Workshop on finite model theory. University of Wales, Swansea (July 1996)Google Scholar
  13. 13.
    Tenzer, J., Stevens, P.: Modelling recursive calls with UML state diagrams. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 135–149. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)Google Scholar
  15. 15.
    von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior, 3rd edn. Princeton University Press, Princeton (1953)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Perdita Stevens
    • 1
  • Jennifer Tenzer
    • 1
  1. 1.Software Engineering Programme and Laboratory for Foundations of Computer Science School of InformaticsUniversity of EdinburghUK

Personalised recommendations