Authors: Pahl, Claus
Title: Grundlagen für die formale Spezifikation modularer zustandsbasierter Systeme
Language (ISO): de
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.
URI: http://hdl.handle.net/2003/2635
http://dx.doi.org/10.17877/DE290R-13051
Issue Date: 1998-03-03
Publisher: Universität Dortmund
Appears in Collections:LS 10 Software-Technologie

Files in This Item:
File Description SizeFormat 
pahl96.pdfDNB1.25 MBAdobe PDFView/Open
ds_Claus_Pahl.ps.gz593.73 kBGNU ZIPView/Open


This item is protected by original copyright



All resources in the repository are protected by copyright.