Grundlagen für die formale Spezifikation modularer zustandsbasierter Systeme

Abstract

Diese Arbeit stellt Konzepte vor, die im Kontext zustands- oder objektbasierter Systeme die gemeinsame Behandlung von Implementierungssprachen und Spezifikationssprachen gestatten. Sie befaßt sich zum einen mit der formalen Definition einer Programmiersprache und zum anderen mit dem Entwurf einer Spezifikationssprache, die auf die Programmiersprache ausgerichtet ist. Abhängigkeiten zwischen diesen beiden Aspekten werden herausgearbeitet. Die Definition beider Sprachen erfolgt auf einem eigenständigen Berechnungsmodell, einer formal definierten abstrakten Maschine, zur Modellierung des Verhaltens von Objekten. Erweiterungen des Berechnungsmodells, die Rekursion, Verschachtelung von Programmeinheiten oder Typfragen betreffen, werden vorgestellt. Zur Spezifikation zustandsbasierter Systeme wird dynamische Logik, eine Erweiterung einer Prädikatenlogik erster Stufe, die Zustände explizit macht, eingesetzt. Mit Hilfe der dynamischen Logik kann das Verhalten von Objekten abstrakt beschrieben werden. Ein Beweissystem für die Logik wird definiert, mit dem auch die Verifikation einer Implementierung bezüglich einer Spezifikation möglich ist. Hierzu wird ein Korrektheitsbegriff definiert, der durch das Beweissystem operationalisiert wird. Zur Beschreibung von modularen Software-Systemen werden formale Parametrisierungs- und Schnittstellenkonzepte erarbeitet. Eine Reihe von Relationen wird definiert, die es ermöglichen, verschiedene Beziehungen zwischen Systemkomponenten zu modellieren. Horizontale und vertikale Entwicklung wird betrachtet.