Keywords:

Keywords:
Astract: With the introduction of OMG's Foundational UML (fUML) standard, that precisely defines the execution semantics for a subset of UML, and the conforming virtual machine, completely executable systems can be built and executed with UML. However, the full potential of having executable models has yet to be unleashed. An important aspect that increases the potential of executable models is the ability to re-use existing software components since that reportedly increases the overall quality and productivity of the software development process. Furthermore, large-scale software that is produced nowadays, involves the usage of a high number of existing software components primarily in form of software libraries (i.e., APIs provided for the used programming language). This thesis identified that the fUML standard does not offer a procedure to use software libraries. In fact, creating models that build on top of software libraries is not foreseen in the fUML standard. On the contrary, the standard foresees its extendability through the Foundational Model Library. Yet, doing so requires implementing model libraries that basically mimic the functionality provided by currently existing software libraries. This approach imposes a significant drawback. It requires a huge amount of dedicated joint effort to build a set of libraries having similar functional coverage and sophistication as the existing set of software libraries. The research question of this thesis is as follows. Is the fUML virtual machine extendable, such that it allows the execution of models referencing external software libraries? Within this work, an approach has been elaborated that enables to use external software libraries in fUML models. The applicability of this approach has been shown by implementing a prototypical Integration Layer that is able to integrate Java libraries with the fUML virtual machine such that the modeler can benefit from the advanced and complex functionalities provided by those libraries. This prototype focuses on creating instances of library classes and calling library operations. Moreover, a two-step procedure to make existing libraries available for their usage in fUML models, has been implemented. While conducting several case studies, experiences have been gained that led to further enhancements of the prototype and to the following conclusion. The fUML virtual machine can be extended, such that it allows the execution of models referencing external libraries. Nevertheless, to broaden the applicability of the implemented prototype, and therefore increase the scope of applicable modeling scenarios, an in-depth investigation on common library use cases and their following implementation is recommended.

Keywords:
Astract: Today, modeling and programming constitute separate activities carried out using modeling respectively programming languages, which are neither well integrated with each other nor have a one-to-one correspondence. As a consequence, platform and implementation details, such as the usage of existing software components and libraries, are usually introduced on code level only. This impedes accurate model-level analyses that take platform-specific decisions into account as well as the direct deployment of executable models on the target platform. In this work we present an approach for integrating existing software libraries with fUML models-an executable variant of UML models for which a standardized virtual machine exists-not only at design time but also at runtime. As a result of that, the modeler is empowered with the capabilities provided by existing software libraries on model level. Our approach is evaluated based on unit tests and initial case studies available in the ReMoDD repository that assess the correctness, performance, and completeness of our implementation.

Keywords: model-driven engineering, verification, model checking
Astract: The aim of this master thesis is to reduce the conceptual gap between software modeling and model checking. While model checking is successfully applied for hardware verification, it is not widespreadly used in model-driven engineering (MDE). Thus, we tried to reduce this gap by combining modeling and model checking concepts. This thesis first describes the history and basic idea of both MDE and model checking with a focus on the technologies used in this thesis. Before presenting our new approach, existing solutions are compared. Most approaches propose to extend the Object Constraint Language (OCL) by temporal aspects. This allows to describe the behavior of a software system additionally to various properties of static models. However, one of the main missing features in general seems to be a user-friendly representation of the verification result helpful for debugging. Often, the technical spaces are changed. With our solution we provide (i) a temporal OCL extension based on the Computational Tree Logic (CTL) and (ii) an OCL extension that introduces path selectors to extract interesting system configurations from the state space. Both OCL extensions were formally defined and implemented. We describe systems in terms of state spaces consisting of EMOF-model states and state transitions containing a mapping between model elements of different states. The system behavior is specified using an initial Ecore model and graph transformations based on the Henshin tool2. The approach, however, is designed to be flexible enough to allow an easy integration of any kind of behavior specification as long as a suitable state space can be derived thereof. Our model checking framework is developed with a focus on delivering not only the results, but also making the system behavior leading to the result comprehensible by providing a suitable tool including a web interface. The implementation was evaluated in terms of performance to find out the maximum evaluable model size and query complexity. Further, a qualitative user study was conducted for evaluating the CTL extension and the tool. The results of this study indicate that both the CTL-based extension of OCL as well as the tool are a promising first step to integrate model checking in the MDE life cycle.

Keywords: