Loading…
Thumbnail Image

Transformation-Based Component Architectures - General Framework, Instantiations and Case Study

Klein, Markus

Die Arbeit stellt ein abstraktes Konzept für die Spezifikation von Softwarekomponenten vor, welches die Spezifikation von Komponenten mit jeweils mehreren anbietenden und fordernden Schnittstellen unterstützt. Die Verbindung von Komponenten ist durch Familien von Transformation zwischen fordernden und anbietenden Schnittstellen definiert. Die Komposition von Komponenten wird mittels Erweiterung und multipler Erweiterung von Transformationen und Transformationsfamilien definiert. Das Konzept beinhaltet eine Semantik für Komponentenarchitekturen durch Reduktion zu einer einzelnen Komponente. Diese Reduktion ist durch die Komposition von Komponenten realisiert. Es wird bewiesen, dass die angegebene Architektursemantik wohldefiniert und eindeutig ist, wenn Erweiterung und multiple Erweiterung von Transformationen, Komposition von Extensionsdiagrammen und disjunkte fordernde Schnittstellen in den Komponenten gegeben sind. Darüberhinaus bietet das Konzept eine Semantik für einzelne Komponenten, deren Verträglichkeit mit der Komposition bewiesen wird. Das Konzept vorgestellte ist primär für eine Instantiierung mit formalen Spezifikationstechniken ausgelegt. Die formale mathematische Semantik solcher Techniken bildet, zusammen mit dem vorgestellten Konzept, einen Ausgangspunkt für die Anwendung formaler Analysetechniken, zum Beispiel formale Verifikation und Model-Checking, auf entsprechende komponentenbasierte Architekturspezifikationen. Trotzdem ist es möglich das Konzept mit Techniken ohne formale mathematische Semantik zu instantiieren. Das vorgestellte Konzept kann als eine Generalisierung von abstrakten hierarchischen und konnektorbasierten Ansätzen zur Architekturspezifikation gesehen werden, da in beiden Fällen gezeigt werden kann, dass es sich um Spezialfälle des Konzeptes in dieser Arbeit handelt. Neben kleineren Beispielen zur besseren Verständlicheit der abstrakten Definitionen und Theoreme, demonstriert eine Fallstudie die Anwendbarkeit des Konzeptes. Dabei werden die Spezifikationstechniken der Elementarnetze und der UML Diagramme angewendet. Dies beinhaltet auch eine Instantiierung des abstrakten Konzeptes mit den jeweiligen Techniken. Desweiteren wird eine Instantiierung für AHLR-Kategorien präsentiert.
The thesis introduces an abstract framework for the specification of software components with multiple require and provide interfaces that allows the specification of multiple access to a single provide interface. Component connections are given by families of transformations connecting require and provide interfaces. Component composition is defined in terms of extension and multiple extension of transformations or transformation families, respectively. It is proven that the result of two composition steps is not affected by the order of calculation. The framework offers a semantics to component architectures by reducing them to components by composition. This semantics is proven to be well-defined and unique if multiple extension and composition of extension diagrams as well as disjoint require interfaces are given. Moreover, the framework offers a semantics for components which is shown to be compositional. The abstract framework is primary meant to be instantiated with formal specification techniques featuring a mathematical semantics, and thus, enabling the application of formal analysis techniques like formal verification and model-checking to component architectures specified by those techniques. Nevertheless, it is also possible to instantiate the framework with specification techniques lacking a formal mathematical semantics. This framework can be regarded as a generalization of abstract hierarchical and connector based architecture specification approaches because both turn out to be special cases of the concept presented here. Besides small examples accompanying the formal definitions and theorems a case study using elementary nets and UML diagrams demonstrates the applicability of the framework. This includes instantiations of the framework for the corresponding techniques. Moreover, the framework is instantiated with adhesive HLR categories.