Zur automatischen Verifikation von UML 2 Aktivitätsdiagrammen

One approach to face the increasing demands on the performance and quality of modern software systems is given by the modeldriven software development (MDSD). The use of models increases the abstraction level in software development and allows an enhancement of productivity by automation. The Unified Modeling Language (UML) version 2 is a wide-spread graphical modeling language applied for this purpose. It defines several diagram types to describe a system from different points of view. Activity diagrams consist of actions which may be connected by control- and objectflows. Control nodes are provided for a more detailed control of flows. These nodes split, merge and join flows or decide among different alternatives. Special actions allow for sending and receiving signals or the consideration of time aspects. Besides the increase of productivity, another advantage of abstraction is verification. Contrary to tests, verification does not only find errors, but it can prove their absence. This thesis presents an approach for model checking of UML 2 activity diagrams. A transformation of these diagrams into a state transition system is developed in order to reuse existing tools. This flexibility concerning the underlying model checker makes it possible to profit by further enhancements in this area of research. Whereas previous approaches cover only few aspects of activity diagrams, this thesis includes more difficult aspects like object flows, signal handling and interruptible activity regions. Additionally, the semantics can be adjusted to individual needs by semantic variation points. The formal results of this thesis are also prototypically integrated into a tool for modeldriven development with UML 2 activity diagrams. The formal results of this thesis are also prototypically integrated into a tool for modeldriven development with UML 2 activity diagrams