This thesis investigates the properties of generic refinements of behavioral specifications. At the base of this investigation stands the view from algebraic specification that abstract data types can be modeled as algebras. A specification of a data type is formed from a syntactic part, i.e. a signature detailing the interface of the data type, and a semantic part, i.e. a class of algebras (called its models) that contains the valid implementations of that data type. Typically, the class of algebras that constitutes the semantics of a specification is defined as the class of algebras that satisfy some given set of axioms. The behavioral aspect of a specification comes from relaxing the requirements imposed by axioms, i.e. by allowing in the semantics of a specification not only the algebras that literally satisfy the given axioms, but also those algebras that appear to behave according to those axioms. Several frameworks have been developed to express the adequate notions of what it means to be a behavioral model of a set of axioms, and our choice as the setting for this thesis will be Bidoit and Hennicker’s Constructor-based Observational Logic, abbreviated COL. Using specifications that rely on the behavioral aspects defined by COL we study the properties of generic refinements between specifications. Refinement is a relation between specifications. The refinement of a target specification by a source specification is given by a function that constructs models of the target specification from the models of the source specification. These functions are called constructions and the source and target specifications that they relate are called the context of the refinement. The theory of refinements between algebraic specifications, with or without the behavioral aspect, has been well studied in the literature. Our analysis starts from those studies and adapts them to COL, which is a relatively new framework, and for which refinement has been studied only briefly. The main part of this thesis is formed by the analysis of generic refinements. Generic refinements are represented by constructions that can be used in various contexts, not just in the context of their definition. These constructions provide the basis for modular refinements, i.e. one can use a locally defined construction in a global context in order to refine just a part of a source specification. The ability to use a refinement outside its original context imposes additional requirements on the construction that represents it. An implementer writing such a construction must not use details of the source models that can be contradicted by potential global context requirements. This means, roughly speaking, that he must use only the information available in the source signature and also any a priori assumption that was made about the contexts of use. We look at the basic case of generic refinements that are reusable in every global context, and then we treat a couple of variations, i.e. generic refinements for which an a priori assumption it is made about the nature of their usage contexts. In each of these cases we follow the same pattern of investigation. First we characterize the constructions that ensure reusability by means of preservation of relations, and then, in most cases, we show that such constructions must be definable in terms of their source signature. Throughout the thesis we use an informal analogy between generic (i.e. polymorphic) functions that appear in second order lambda calculus and the generic refinements that we are studying. This connection will enable us to describe some properties of generic refinements that correspond to the properties of polymorphic functions inferred from their types and named “theorems for free” by Wadler. The definability results, the connection between the assumptions made about the usage contexts and the characterizing relations, and the “theorems for free” for behavioral specifications constitute the main contributions of this thesis.

Requirements engineers have to elicit, document, and validate how stakeholders act and interact to achieve their common goals in collaborative scenarios. Only after gathering all information concerning who interacts with whom to do what and why, can a software system be designed and realized which supports the stakeholders to do their work. To capture and structure requirements of different (groups of) stakeholders, scenario-based approaches have been widely used and investigated. Still, the elicitation and validation of requirements covering collaborative scenarios remains complicated, since the required information is highly intertwined, fragmented, and distributed over several stakeholders. Hence, it can only be elicited and validated collaboratively. In times of globally distributed companies, scheduling and conducting workshops with groups of stakeholders is usually not feasible due to budget and time constraints. Talking to individual stakeholders, on the other hand, is feasible but leads to fragmented and incomplete stakeholder scenarios. Going back and forth between different individual stakeholders to resolve this fragmentation and explore uncovered alternatives is an error-prone, time-consuming, and expensive task for the requirements engineers. While formal modeling methods can be employed to automatically check and ensure consistency of stakeholder scenarios, such methods introduce additional overhead since their formal notations have to be explained in each interaction between stakeholders and requirements engineers. Tangible prototypes as they are used in other disciplines such as design, on the other hand, allow designers to feasibly validate and iterate concepts and requirements with stakeholders. This thesis proposes a model-based approach for prototyping formal behavioral specifications of stakeholders who are involved in collaborative scenarios. By simulating and animating such specifications in a remote domain-specific visualization, stakeholders can experience and validate the scenarios captured so far, i.e., how other stakeholders act and react. This interactive scenario simulation is referred to as a model-based virtual prototype. Moreover, through observing how stakeholders interact with a virtual prototype of their collaborative scenarios, formal behavioral specifications can be automatically derived which complete the otherwise fragmented scenarios. This, in turn, enables requirements engineers to elicit and validate collaborative scenarios in individual stakeholder sessions – decoupled, since stakeholders can participate remotely and are not forced to be available for a joint session at the same time. This thesis discusses and evaluates the feasibility, understandability, and modifiability of model-based virtual prototypes. Similarly to how physical prototypes are perceived, the presented approach brings behavioral models closer to being tangible for stakeholders and, moreover, combines the advantages of joint stakeholder sessions and decoupled sessions. / Anforderungsingenieure erheben, dokumentieren und validieren wie Bedarfsträger in einzelnen und gemeinsamen Aktivitäten die Ziele ihrer kollaborativen Szenarios erreichen. Auf Grundlage von Angaben darüber, wer warum mit wem zusammen was erledigt, kann anschließend ein Softwaresystem spezifiziert und umgesetzt werden, welches die Bedarfsträger bei der Durchführung ihrer Abläufe unterstützt. Um Anforderungen verschiedener (Gruppen von) Bedarfsträger zu erfassen und zu strukturieren, werden szenariobasierte Ansätze genutzt und erforscht. Die Erhebung und Validierung von Anforderungen, die kollaborative Szenarios abdecken, ist dennoch kompliziert, da derartige Informationen hochgradig verknüpft, fragmentiert und über mehrere Bedarfsträger verteilt sind, wodurch sie nur in Gruppensitzungen effizient erhoben und validiert werden können. In Zeiten global verteilter Firmen ist die Planung und Durchführung solcher Workshops mit Gruppen von Bedarfsträgern nur selten praktikabel. Mit einzelnen Bedarfsträgern zu sprechen ist hingegen oft realisierbar, führt aber zu fragmentierten, unvollständigen Szenariobeschreibungen. Durch eine Vielzahl von Einzelgesprächen mit wechselnden Bedarfsträgern kann diese Fragmentierung aufgelöst werden – dies ist aber eine fehleranfällige und zeitaufwändige Aufgabe. Zwar bieten formale Modellierungsmethoden z.B. automatische Konsistenzchecks für Szenarios, doch führen derartige Methoden zu Mehraufwand in allen Gesprächen mit Bedarfsträgern, da diesen die verwendeten formalen Notationen jedes Mal erläutert werden müssen. Handfeste Prototypen, wie sie in anderen Disziplinen eingesetzt werden, ermöglichen es Designern, ihre Konzepte und erhobenen Anforderungen ohne viel Aufwand mit Bedarfsträgern zu validieren und zu iterieren. In dieser Dissertation wird ein modellbasierter Generierungsansatz vorgeschlagen, der kollaborative Szenarios prototypisch auf Grundlage von formalen Verhaltensmodellen für die beteiligten Bedarfsträger darstellt. Durch die Simulation dieses Verhaltens und dessen Animation innerhalb einer webbasierten, domänenspezifischen Visualisierung, können Bedarfsträger diese Modelle erleben und die bisher erfassten Szenarios validieren. Eine derartige interaktive Szenariosimulation wird als modellbasierter virtueller Prototyp bezeichnet. Basierend auf den Interaktionen zwischen Bedarfsträgern und einem virtuellen Prototypen ihrer Szenarios können zudem formale Verhaltensspezifikationen automatisch abgeleitet werden, die wiederum die fragmentierten kollaborativen Szenarios vervollständigen. Dies ermöglicht es den Anforderungsingenieuren, die kollaborativen Szenarios in individuellen Sitzungen mit einzelnen Bedarfsträgern zu erheben und zu validieren – entkoppelt voneinander, da Bedarfsträger webbasiert teilnehmen können und dabei nicht darauf angewiesen sind, dass andere Bedarfsträger ebenfalls in der gleichen Sitzung teilnehmen. Diese Dissertation diskutiert und evaluiert die Machbarkeit, Verständlichkeit sowie die Änderbarkeit der modellbasierten virtuellen Prototypen. Auf die gleiche Art wie physikalische Prototypen wahrgenommen werden, erlaubt es der vorgestellte Ansatz, Verhaltensmodelle für Bedarfsträger erlebbar zu machen und so die Vorteile von Gruppensitzungen mit denen entkoppelter Sitzungen zu verbinden.

First, this thesis presents an analysis of diversity of component-based software engineering (CBSE) concepts and approaches, and provides a summary of selected runtime-aware component models structured according to newly proposed criteria. As a result of the analysis, hierarchical component models are identified as a CBSE domain still not sufficiently explored in the current research with respect to their lacking penetration into regular industrial use. The major part of the thesis consequently almost exclusively focuses on problems related to application of hierarchical component models to real-life applications development. The motivations for hierarchical structuring of application architectures are presented in the thesis and key advantages of hierarchical component models are thoroughly discussed and shown on examples from commercial software development. To verify the claims, two major case-studies are presented in the thesis and the Fractal component model is successfully applied to model and implement them focusing on formal verifiability of correctness of resulting component-based applications. The thesis proposes novel approaches to model dynamic architectures changing at runtime, to deal with complex error traces and a novel specification language for component environments, all resulting from...