Keywords: EMF Profiles, UML, DSMLs, extension mechanism, GMF
Astract: EMF Profiles is an adaptation of the well-known Unified Modeling Language (UML) profile concept to Domain Specific Modeling Languages (DSML). Profiles have been a key enabler for the success of UML by providing a lightweight language-inherent extension mechanism which is expressive enough to cover an important subset of adaptation scenarios. Thus, we believe a similar concept for DSMLs provides an easier extension mechanism that has been so far neglected by current metamodeling tools. The Profile mechanism is based on a profile definition comprised of stereotype definitions. Stereotypes are used to annotate model elements in order to refine their meta-classes by defining supplemental information in form of additional meta attributes, also known as tag definitions. Instances of tag definitions are known as tagged values and they are used for the provision of new informations to existing models. With EMF Profiles, users can apply profiles within graphical modeling editors that are created using the Graphical Modeling Framework (GMF). Applied stereotypes are visualized using icons that are attached to shapes that represent the model elements to which stereotypes are applied. However, in many scenarios, visualization methods going beyond simple icons are helpful for locating and grasping the applied stereotypes and to allow for more domain-specific decorations according to the domain of the applied profile. For instance, highlighting a shape by a specific background color or enriching the shape with adornments and informations from a stereotype application reflects the meaning of the stereotype application more adequately than a simple icon. This thesis aims at providing decoration methods for applied stereotypes in EMF Profiles going beyond simple icons.

Keywords:
Astract: This textbook mainly addresses beginners and readers with a basic knowledge of object-oriented programming languages like Java or C#, but with little or no modeling or software engineering experience - thus reflecting the majority of students in introductory courses at universities. Using UML, it introduces basic modeling concepts in a highly precise manner, while refraining from the interpretation of rare special cases. After a brief explanation of why modeling is an indispensable part of software development, the authors introduce the individual diagram types of UML (the class and object diagram, the sequence diagram, the state machine diagram, the activity diagram, and the use case diagram), as well as their interrelationships, in a step-by-step manner. The topics covered include not only the syntax and the semantics of the individual language elements, but also pragmatic aspects, i.e., how to use them wisely at various stages in the software development process. To this end, the work is complemented with examples that were carefully selected for their educational and illustrative value. Overall, the book provides a solid foundation and deeper understanding of the most important object-oriented modeling concepts and their application in software development. An additional website (www.uml.ac.at) offers a complete set of slides to aid in teaching the contents of the book, exercises and further e-learning material.

Keywords: Model Engineering, Standardization, UML, fUML, Enterprise Architect
Astract: The rise of Model Driven Development (MDD) has renewed the interest in the execution of models. The predominant modeling language applied in MDD is the Unified Modeling Language (UML). Unfortunately, UML lacks clear execution semantics. This has lead to a plethora of different interpretations both in academia and industry, hindering the interoperability of UML tools supporting the execution of models. A possible solution to this problem is the so-called Foundational Subset For Executable UML Models (fUML) standard published by the Object Management Group (OMG). fUML is an extension of UML, defining a standardized execution semantics for a subset of UML. fUML has, however, not yet been widely adopted in commercial tooling. This thesis investigates the integration of fUML with existing commercial UML modeling tools to contribute to the adoption of fUML and identify challenges arising in the integration. To this end, this thesis aims to answer the following research questions: 1. Can fUML be integrated into a proprietary UML model execution environment? Which challenges arise in the integration? 2. Does the standardized fUML model execution environment provide the same functionality as a proprietary UML model execution environment? 3. Is the performance of the standardized fUML model execution environment comparable to the performance of a proprietary UML model execution environment? To explore these questions, a prototypical integration of fUML into the commercial UML modeling tool Enterprise Architect (EA) has been implemented in this thesis. The goal of the prototype is to allow execution and debugging of UML state machines and sequence diagrams via EA-s execution environment, in conjunction with the execution of UML activity diagrams via the fUML execution environment. The evaluation of the prototype has shown that the integration of the execution environments has been completed successfully. The prototype is capable of executing and debugging state machines, sequence diagrams and fUML compliant activity diagrams in conjunction, while still providing the same functionality as the proprietary execution environment. The performance analysis has shown that the prototype is slower than the proprietary execution environment provided by EA. This is mostly due to the necessity of running two different execution environments in parallel.

Keywords: Model Checking, Model Driven Software Development
Astract: In today's software, no matter how security and safety critical it may be, defects and failures are common. With the rising complexity of software and our growing dependency on its correct functioning as it permeates our every day life the software development process requires new approaches to integrate formal verification techniques. This thesis presents approaches on efficiently verifying software systems described by model-driven software development artifacts. These artifacts comprise the implementation of the system and consist of both structural and behavioral models. We present two model checking approaches, MocOCL and Gryphon, to verify the temporal specification of a system against its model-based implementation. Central to our approach is the twofold use of graphs to describe the system under verification. First, we describe the admissible static structure of an instance of the system by means of attributed type graphs with inheritance and containment relations, often referred to as metamodel. Second, we represent a state of the system as an object graph that enumerates a system's active objects, the references among them, and their attribute values. A change in the system, e.g., the deletion of an object or the modification of an attribute value, triggers a state change. The behavior of the system is thus described by actions that modify the state of the system. In this thesis we employ graph transformations to model such state-changing actions as they provide suitable means to formally describe modifications on graphs. The specification of the system, on the other hand, is written in our temporal extension of the Object Constraint Language (OCL) that is based on Computation Tree Logic (CTL). A specification written in our CTL extension for OCL, called cOCL, can be verified against a model-based implementation of the system with our explicit-state model checker MocOCL. Gryphon aims to increase the efficiency and scalability of the verification process and implements a symbolic model checking approach, that focuses the verification on safety specifications. The work presented in this thesis also encompasses a survey and a feature-based classification of verification approaches that can be used to verify artifacts of model-driven software development. Methodologically, it provides the motivation for our work on MocOCL and Gryphon. Both our approaches are novel in their own respect; MocOCL for its capability to verify CTL-extended OCL expressions and Gryphon for its use of relational logic to build a symbolic representation of the system that can be verified with any model checker participating in the Hardware Model Checking Competition. Finally, MocOCL and Gryphon are evaluated performance-wise on a set of three representative benchmarks that demonstrate the model checkers' preferred fields of application and its limitations.

Keywords: