Executable HybridUML Semantics.A Transformation Definition.

Abstract

This thesis contributes to the development of hybrid systems. For the particular specification formalism HybridUML, a formally defined transformation Phi of HybridUML models into executable low-level models is defined. The resulting low-level models have a formal semantics, therefore by Phi, this formal semantics is assigned to the corresponding HybridUML models. As a result, there is no inconsistency between the HybridUML specification of a hybrid system and its implementation. HybridUML is derived from the Unified Modeling Language, which is a wide-spread modeling language for the development of software systems. The semantics is executable, i.e. executable code is automatically generated from HybridUML models, such that they are directly usable in practice.Chapter 1 motivates the use of the specification formalism HybridUML for the formal definition of hybrid systems. As an approach to combine the definition of hybrid systems in a formal, but user-friendly way, with the generation of a resulting executable system that has formally defined behavior, a transformation concept is proposed: Hybrid systems models are modeled with the specification language HybridUML, and are transformed into programs of the Hybrid Low-Level Framework HL3, which provides a restricted design pattern that the transformation has to comply with, as well as a runtime environment that provides basic functionality.Chapter 2 defines the HybridUML Mathematical Meta-Model, which is a non-graphical definition of the HybridUML syntax. The separation of the meta-model from its graphical representation is the usual UML approach, and the benefits are that (1) the meta-model is directly usable for transformation Phi, and that (2) the HybridUML semantics is independent from the graphical notation. In chapter 3, the expressions that can be used within a HybridUML model, e.g. boolean expressions from mode invariants or transition conditions, or assignment expressions from transition actions, are defined by means of the HybridUML Expression Language.The HL3 Low-Level Framework is discussed in chapter 4. It is a compilation target for hybrid systems specification formalisms. A formal operational semantics is given for the execution of HL3 models, which are defined as a mixture of explicit program code and abstractions to mathematical representations.The specific transformation Phi_HUML from HybridUML models to instances of the HL3 framework is presented in chapter 5. The transformation is defined formally, therefore the HybridUML executable semantics results.The thesis is concluded in chapter 6. A summary is given, and the main scientific contributions are pointed out. Possible future work related to HybridUML, to the low-level framework HL3, and to the transformational approach is discussed.