Formal Specification and Rule-Based Refinement of Software Components

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.

Author dc:creator

• Padberg, Julia

Advisor dc:contributor.advisor

• Ehrig, Hartmut

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Language dc:language.iso

en, English

Identifier URI

urn:nbn:de:kobv:83-opus-12658
http://dx.doi.org/10.14279/depositonce-1420

OAI identifier oai:identifier

oai:depositonce.tu-berlin.de:11303/1717