Foundations of a Module Concept for Distributed Object Systems
This thesis provides a logical and mathematical foundation for object-oriented specification languages with a further modularisation unit between the system and object classes. The unit is denoted object-oriented module, or module for short, and initially described in an informal way. Modules offer a better approach to reusability and provide better structuring of large, complex and distributed systems. In our approach, systems and single modules are represented by theory presentations in a module logic. These presentations, also called module specifications, are pairs consisting of a module signature and a set of module axioms. The axioms are formulae in a newly developed module logic MDTL (Module Distributed Temporal Logic). This is a true-concurrent branching-time discrete distributed first-order temporal logic that is interpreted over labelled event structures. Winskel et al. introduced certain event structure morphisms to organise event structures into a category ev with limits. Here we present a second notion of morphism between event structures, so-called communication event structure morphisms, that result in a different category cev with just the right colimits for our purposes. Crucially, in some cases a morphism in ev has a corresponding reverse morphism in cev. A categorical construction is presented which uses limits in ev and colimits in cev. The construction may be used to model several module operations in a uniform way. In particular, we consider concurrent composition (synchronous, asynchronous, or mixed), parameter actualisation, refinement, restriction (hiding) and renaming.
Diese Arbeit liefert eine logische und mathematische Grundlage für objektorientierte Spezifikationssprachen mit einer weiteren Modularisierungsebene zwischen einem System und Objektklassen. Elemente dieser Ebene werden objektorientierte Module, oder kurz Module, genannt und in dieser Arbeit zunächst informell beschrieben. Module ermöglichen eine bessere Form der Wiederverwendung und Strukturierung von großen, komplexen und verteilten Systemen. In unserem Ansatz werden Systeme und Module als Theorie-Präsentationen einer Modullogik dargestellt. Die Präsentationen, auch Modulspezifikationen genannt, sind Paare, die eine Modulsignatur und eine Menge von Modulaxiomen beinhalten. Die Axiome sind Formeln in einer neu entwickelten Modullogik MDTL (Module Distributed Temporal Logic). MDTL ist eine echt-nebenläufige zeit-verzweigte diskrete verteilte temporale Logik erster Stufe, die auf markierten Ereignisstrukturen interpretiert wird. Winskel et al. führten bestimmte Morphismen ein, um die Ereignisstrukturen als Kategorie mit Limiten auffassen zu können. Hier stellen wir einen zweiten Morphismenbegriff für Ereignisstrukturen vor, sogenannte Kommunikationsmorphismen, die zu einer anderen Kategorie mit gerade den von uns benötigten Colimiten führen. Besonders wichtig ist, daß in bestimmten Fällen ein Morphismus in ev einen entsprechenden Morphismus in der Gegenrichtung in cev hat. Wir beschreiben eine kategorielle Konstruktion, die Limiten in ev und Colimiten in cev benutzt. Sie ermöglicht die semantische Beschreibung diverser Moduloperationen in einer einheitlichen Form. Speziell betrachten wir nebenläufige Komposition (synchron, asynchron oder beides), Parameteraktualisierung, Verfeinerung, Restriktion und Umbenennung.
Preview
Cite
Access Statistic
Rights
Use and reproduction:
All rights reserved