Ziel der Arbeit ist es, die Grundlagen für ein modulares Spezifizieren nebenläufiger Systeme mit Petrinetzen zu legen und das modulare Analysieren von Systemeigenschaften zu ermöglichen. Dabei liegt der Schwerpunkt auf der Entwicklung der dazu notwendigen Theorie, deren Praxisbezug aber stets erkennbar bleibt. Mit den Algebraischen High-Level-Netzen erweitern wir eine der für praktische Anwendungen geeignetsten Petrinetzklassen und bringen sie, durch die Einführung von Kompositions- und Parameterisierungsoperationen, dem Einsatz im Bereich nebenläufige Systeme einen wesentlichen Schritt näher. Den einheitlichen Rahmen für Spezifikationen und deren Semantik bilden Konstruktionen der Kategorientheorie. Grundlage dür das Verstehen und Analysieren von Systemen ist die Unterscheidung zwischen Spezifikationen als abstrakte Beschreibungen notwendiger Eigenschaften und deren Konkretisierung in Form von Modellen. Dabei sollen alle spezifizierten Eigenschaften in den Modellen nachweisbar und alle implementierungsbedingten Anpassungen möglich sein. Im Unterschied zu der in der Literatur üblichen Modellbildung, die zwar eine Variation des Datentypanteils in Form verschiedener Algebren zulässt, aber die Netzstruktur unverändert in jedes Modell übernimmt, interpretieren wir beide Teile einer Systemspezifikation lose. Für das übliche asymmetrische Vorgehen gibt es in der Literatur weder inhaltliche noch anwendungsbezogene Begründungen. Ob eine Spezifikation das gewünschte Verhalten beschreibt, ist nur mit Hilfe von Modellen nachweisbar, die neben den spezifizierten Eigenschaften über keine weiteren verfügen. Ein derartiges initiales Modell ist im Rahmen unseres Ansatzes für jede Spezifikation konstruierbar. Um eine detaillierte Beschreibung der in einem System möglichen Abläufe zu erhalten, ordnen wir jedem Spezifikationsmodell eine operationale Semantik in Form von Prozesstermen zu. Diese kompositionale "true concurrency" Semantik stellt das für die Petrinetztheorie essentielle Verhältnis von Nichtdeterminismus und Nebenläufigkeit in den Vordergrund und lässt sich direkt in die übliche Prozessdarstellung übertragen. Systeme in der Praxis sind meist deutlich komplexer als die im Bereich der Petrinetztheorie verwendeten Beispiele. Sie erfordern daher, neben einer eindeutigen Spezifikation, Möglichkeiten zu deren strukturierter Erstellung. Die hier eingeführten Kompositions- und Parameterisierungsoperationen, mit ihren bis auf Isomorphie eindeutigen Ergebnissen, schaffen dafür die Grundlagen. Ihnen stehen entsprechene Eigenschaften auf Seiten der Modell- und Prozesstermsemantik gegenüber, ohne die ihr Nutzen für die Praxis stark eingeschränkt wäre.
«
Ziel der Arbeit ist es, die Grundlagen für ein modulares Spezifizieren nebenläufiger Systeme mit Petrinetzen zu legen und das modulare Analysieren von Systemeigenschaften zu ermöglichen. Dabei liegt der Schwerpunkt auf der Entwicklung der dazu notwendigen Theorie, deren Praxisbezug aber stets erkennbar bleibt. Mit den Algebraischen High-Level-Netzen erweitern wir eine der für praktische Anwendungen geeignetsten Petrinetzklassen und bringen sie, durch die Einführung von Kompositions- und Paramete...
»
Login
BibTeX