Formale Spezifikation und regelbasierte Verfeinerung von Software-Komponenten

Software-Komponenten stellen einen allgemein anerkannten Abstraktionsmechanismus dar, der während des gesamten Lebenszykluses eines Software-Systems von der Analyse bis zur Wartung eingesetzt wird. Komponentenbasierte Software-Entwicklung benötigt formale Konzepte und Modellierungstechniken, da die hohe Komplexität solcher Systeme häufig die Konsistenz dieser beeinträchtigt. Diese Komplexität resultiert im Wesentlichen aus der nichtdeterminierten und nebenläufigen Interaktion der Komponenten und ist auch ein Haupthindernis für die Anpassung an sich ändernde Systemumgebungen. Also ist eine formale Komponententechnik, wie sie in dieser Schrift vorgestellt wird und die die formale Komponentenbeschreibung, ihre Semantik, Kompositionsoperationen sowie die Verfeinerungskonzepte umfasst, nötig für die formale Fundierung der komponentenbasierten Entwicklung. Für die präzise Komponentenbeschreibung ist eine passende Syntax und für die mathematische Argumentation eine formale Semantik erforderlich. Die formale Beschreibung der Komponentenschnittstellen sowie der Komponentenspezifikation erlaubt die gründliche mathematische Modellierung und die Verifikation der gewünschten Funktionalität. Darüber hinaus stellen Kompositionsoperatoren Korrektheit und Konsistenz sowohl für Basiskomponenten als auch für zusammengesetzte Komponenten sowie das gesamte komponentenbasierte System sicher. Unterschiedliche Kompositionsoperationen erhöhen die Flexibilität während der Entwicklung des Systems. Komponentenbasierte Softwareentwicklung und -wartung braucht Verfeinerungskonzepte als eine formale Basis für die Veränderung von Komponenten in ihrer Umgebung. Die Verträglichkeit der Komponentenverfeinerung mit den Komponentenoperationen ist eine zentrale Frage der Veränderung von Komponenten in einem gegebenen Umfeld, so dass Inkonsistenz vermieden wird. Ausgangspunkte der umfassenden, formalen Komponententechnik, die in dieser Schrift beschrieben wird, sind zwei etablierte Theorien: HLR-Systeme (High-Level Replacement) und der transformationsbasierte Rahmen für generische Komponenten. HLR-Systeme sind eine abstrakte Theorie zur Beschreibung der Ersetzung von Objekten in beliebigen Kategorien und stellen eine Verallgemeinerung des Double-Pushout-Ansatzes der Graphtransformationssysteme für beliebige Kategorien dar. Die fundamentalen Konzepte des transformationsbasierten Rahmens sind Komponenten mit Export- und Importschnittstellen, die Komponentensemantik und die hierarchische Komposition. In dieser Schrift stellen wir eine formale Komponententechnik dar, die auf dem transformationsbasierten Rahmen beruht, diesen aber kategoriell formalisiert. Also, gibt es Komponenten mit Export- und Importschnittstellen und einer expliziten Komponentenspezifikation, dem so genannten Body. Wir liefern zwei Semantiken, eine modellbasierte und eine transformationsbasierte. Die erste ist konstruktiv, verlangt aber, dass die zugrunde liegende Spezifikationstechnik ebenfalls eine Modellsemantik hat. Liegt diese nicht vor, dann gibt es die transformationsbasierte Semantik, die jede Transformation des Imports auf eine Transformation des Exports abbildet. Diese Semantik ist jedoch nur funktional, bezieht aber dafür die Umgebung der Komponente mit ein. Die Komposition von Komponenten wird durch zwei Komponentenoperationen, nämlich Union und hierarchische Komposition, sichergestellt. Die Union beschreibt das Verkleben zweier Komponenten entlang einer gemeinsamen Unterkomponente. Die hierarchische Komposition beschreibt, wie eine Komponente eine andere, deren Export dem Import der ersten entspricht, benutzt. Die Verträglichkeit der Operationen ist sichergestellt. Die Kategorientheorie ist dafür die Grundlage und so hat diese Theorie den gleichen Abstraktionsgrad wie die der HLR-Systeme. In beiden Fällen gibt es eine zugrunde liegende Spezifikationskategorie zusammen mit einigen Annahmen über diese Kategorie, jedoch ohne die genaue Spezifikationstechnik festzulegen. Die Kombination dieser Theorien erlaubt die Entwicklung von Komponententransformationen, regelbasierter Verfeinerung für Komponenten und der entsprechenden Resultate. Grundsätzlich wird die Transformation von Komponenten durch die Transformation des Export, des Import und des Bodys in der zugrundeliegenden Spezifikationkategorie erreicht. Wir diskutieren unterschiedliche Instantiierungen, wie algebraische Spezifikationen, Automaten, Petrinetze und Graphtransformationssysteme. Petrinetztransformationen und Petrinetzmodule werden tiefergehend untersucht, um darzustellen, dass diese Konzepte, die aus der Datentypspezifikation stammen, auch für Prozessspezifikationen geeignet sind. Nichtsdestotrotz sind die Begriffe und Ergebnisse auch in den anderen Instantiierungen verfügbar.Software components are a useful and widely accepted abstraction mechanism during the entire software life cycle from analysis to maintenance. They need to be backed by thorough formal concepts and modeling techniques, because the high complexity of component-based systems often impedes its consistency. The high complexity is caused mainly by the non-deterministic and concurrent interaction of components. These also lead to strong dependencies between a component and its environment. This is one main obstacle for the adaption of component-based systems to changing environments. So, a formal component technique, consisting of the component description, semantics, composition operations and refinement concepts, is required for the formal foundation of component-based engineering. Such a component techniques is presented in this thesis. For the precise description of a component a suitable syntax is required, for mathematical reasoning about components a formal semantics is needed. The formal specification of the component interfaces and the component specification allows the rigorous mathematical modeling and the verification of the desired functionality. Moreover, formal component operations and their compatibility with the semantics ensure correctness and consistency not only for basic components but for composed components as well as for the entire component-based system. Different composition operations increase the flexibility when building the system. Component-based software development and maintenance need refinement concepts as a formal foundation for changing the components in the component's environment. The compatibility of component transformation with component operations is a key question of changing components in a given context, so that inconsistencies can be avoided. Starting points for this comprehensive, formal component technique are two well established theories: High-level replacement systems and the transformation-based framework for generic components. High-level replacements systems are an abstract theory for the transformation of objects in an arbitrary category. They are a generalization of the double pushout approach to graph transformations for arbitrary categories. The fundamental concepts in the transformation-based framework for generic components are the import and export interfaces, the compositionality of components and their semantics. In this thesis we present a formal component technique, that is based on the transformation-based framework for components, but that formalizes that framework by using category theory. So we have components with export and import interfaces as well as an explicit component specification, called the body. We supply two kinds of semantics, a model-based semantics and a transformation-based semantics. The first one is constructive but requires a model semantics of the underlying specification technique. If that is not available, there is the transformation-based semantics of component, that maps each transformation of the import to a transformation of the export. This semantics is functional, but it takes directly the environment into account. For the composition of components we have two different operations, namely union and hierarchical compostion