Improving UML design tools by formal games

The Unified Modeling Language (UML) is a standard language for modelling the design of object oriented software systems. The currently available UML design tools mainly provide support for drawing the UML diagrams, i.e. for recording a chosen design, but not for choosing a design. The design of a system is a non-trivial, iterative process and errors which are introduced at this level are usually very expensive to fix. Hence we argue that UML design tools should provide more support for the design activity as such. Ideally a UML design tool should allow the modeller to explore different design options, provide feedback about the design in its current state, and even make suggestions for improvements where this is possible. The usage of such a tool would be highly interactive and very much like a game, played repeatedly between modeller and tool. We claim that this similarity makes formal games a natural and intuitive choice for the definition of tool concepts. Since formal games can be used for verification, a game-based tool can provide feedback about flaws in the design that is formally founded. Games as used in verification normally require a complete formal model of the software system, and a formal specification of the property that is to be verified. Instead of this we would like to let the designer play a game directly on the basis of the UML model, even though a UML model is often incomplete and informally defined. We also want to allow the modeller explore variations of the design while the game is being played. The research hypothesis for this work is that formal games are a suitable technique for more advanced UML design tools which point the modeller to flaws in the design, help to improve the design and provide support for making design decisions.