Welcome to the UML 2 Semantics Project website. The UML 2 Semantics Project is an international collaboration between academia and industry whose main objective is to develop a mathematically formalized semantics definition for the Unified Modeling Language (UML).

Motivation

UML has become the language of choice for modeling various aspects of software systems in academia and industry. The current version of the standard specifically supports model-driven development (MDD), an approach to software development that has the potential to increase the productivity of industrial software development substantially. The proposed formalization of UML will have several benefits. First, it will allow subtle errors in the current and future versions of the standard to be detected and suggestions for improvement to be made. Second, the formalization will have the potential to be of immediate, commercial utility to the companies developing tools supporting UML and MDD. For instance, it would enable tool vendors to develop tools that offer more powerful and effective testing, analysis, and model transformation functionality and better support the exchange of modeling artifacts between different tools.

Major Objectives

  1. To specify a definitive and complete formal semantics foundation for the UML 2 standard.
  2. To identify potential consistency flaws in the UML 2 standard and propose adequate corrections.
  3. To identify analysis techniques that can be used to formally determine the correctness of UML 2 models.
  4. To provide a strong foundation for the definition of a UML virtual machine that is capable of executing UML 2 models.

Methodology and Approach

Our research plan is divided into two sequential phases, each one approximately a year in duration. The first major objective, the development of a formal semantics, provides the foundation for the remaining objectives. These objectives, however, are fairly independent and can be worked on concurrently. The structure of each phase are as follows:

Phase 1 (Foundations and Exploration):

  1. A workable model of the basic structure and behavioural concepts of UML will be defined. An initial formalization of the semantics is provided.
  2. During the development of the initial formalization, a list of potential problems (e.g., imprecision, inconsistencies, and incompleteness) in the official UML standard is compiled.
  3. A list of analysis techniques for UML models is compiled. The techniques will be based on the formalization and may employ existing formal analysis techniques such as static analysis, model checking, or theorem proving. If necessary, new techniques may also be developed. Prototype tools may be developed to evaluate proposed techniques with respect to, e.g., scalability or usability.
  4. The definition of a UML virtual machine for executing UML models is investigated.

Phase 2 (Finalization, Extension, and Validation):

  1. The initial formalization of the semantics from Phase 1 is completed.
  2. The applicability of the semantics to higher-level UML behavioural formalisms is investigated.
  3. Based on the list of analysis techniques developed in Phase 1, a strategy for formal analyses of UML models is defined. An appropriate tools framework is devised by experimenting with existing industrial tools (from IBM and other companies) and, where necessary, with prototype tools based on, for instance, open source model checkers.
  4. A complete UML virtual machine for the execution of UML models is defined.

The work will be carried out as a collaboration between three groups at IBM (Kanata, Munich, and Haifa) and two academic groups (Technical University of Munich and Queen’s University). Each of these groups is able to contribute different, crucial expertise. For instance, the IBM group in Kanata has in-depth knowledge of the UML 2 standard and long experience in modeling different industrial software applications; the group at Technical University of Munich has expertise in formalization of software systems and modeling languages; the group at Queen’s University has background in formal analysis techniques and methods. Moreover, based on the interest expressed, it is anticipated that the core team will be expanded later to include additional academic partners from Canada as well as industrial partners from both Germany and Canada. A number of graduate students and at least one postdoctoral researcher will participate in the project at both academic institutions. Two workshops will be held to solicit input from the general research community and to disseminate results.