Verfeinerung von Zustandsübergangssystemen,
ein uniformer Ansatz basierend auf Ko-Algebren

Zusammenfassung

Basierend auf einer Formalisierung von endlichen und unendlichen Sequenzen als finaler Ko-Algebra (siehe z.B. Rutten : Universal coalgebra: a theory of systems ) wird in dieser Arbeit eine Beschreibung von nichtdeterministischen Zustandsübergangssystemen in PVS angegeben. Die dadurch erzielte uniforme Behandlung von endlichen und unendlichen Abläufen erleichtert die formale Definition und Untersuchung von Verfeinerungsbeziehungen. Dies wird hier an verschiedenen Beispielen dargestellt, insbesondere an einem auf Übergängen und einem auf sichtbaren Zuständen beruhenden Verfeinerungsbegriff. Bei der Untersuchung dieser Begriffe wurde besonderer Wert auf die Entwicklung von hinreichenden lokalen Beweiskriterien gelegt. Eine zentrale Rolle spielen dabei invariante Eigenschaften der Systeme sowie wohlfundierte Ordnungen. Letztere werden als Verallgemeinerung der bekannten Technik für Terminierungsargumente verwendet, um die enthaltenen Lebendigkeitsanforderungen nachzuweisen. Um die Komposition verschiedener Verfeinerungsbeziehungen zu ermöglichen, wird zusätzlich ein verallgemeinerter Begriff eingeführt. Er erlaubt dem verfeinerten System beliebige Zwischenschritte, sofern die Fairneß und damit z.B. auch die Terminierung erhalten bleibt. Ein abschließendes Beispiel demonstriert die Anwendung der entwickelten Theorie anhand einer Variante des Problems der kürzesten Wege, die in einer Arbeit von Karl Stroetmann beschrieben wird. Der Algorithmus von Moore und Ford wird in zwei Verfeinerungsschritten aus der Problemspezifikation entwickelt und als korrekt und terminierend nachgewiesen. Mit Hilfe der lokalen Kriterien konnten die Beweise effizient ohne die sonst übliche Betrachtung ganzer Abläufe geführt werden. Sowohl die dargestellte allgemeine Verfeinerungstheorie als auch das behandelte Beispiel sind mit Hilfe von PVS entwickelt und verifiziert worden. Als Basis für die benötigte ko-algebraische Sequenzentheorie diente die Arbeit A Coalgebraic Theory of Sequences in PVS von Hensel und Jacobs , die für diesen Zweck erweitert und im Hinblick auf Praktikabilität weiterentwickelt wurde.

Online Kopie

Die komplette Arbeit ist derzeit leider nur auf Deutsch erhältlich (fbartels-dipl.ps.gz (330K)), in englischer Sprache ist die Folienvorlage einer kurzen Präsentation des Beispieles verfügbar (ShortestPath.ps.gz (140K)). Die PVS-Formalisierung wird in Kürze ebenfalls hier zu beziehen sein.

BibTeX Eintrag

@MastersThesis{Bartels99,   author = "Falk Bartels",   title = "{Verfeinerung von Zustands{\"u}bergangssystemen,   ein uniformer Ansatz basierend auf Ko-Algebren}",   school = "Universit{\"a}t Ulm",   year = 1999}