Hierarchische Spezifikation und Korrektheitsbeweis eines
parallelen Garbage Collectors
Hans Stadtherr
Diplomarbeit
Institut für Informatik
Technische Universität München
1991
Zusammenfassung.
In dieser Arbeit wird ein nebenläufiger Garbage Collector als
Petrinetz modelliert und formal verifiziert.
Besondere Aufmerksamkeit wird dabei der Adäquatheit der Modellierung
und der Beweistechnik geschenkt.
Im einführenden Teil legen wir unser Augenmerk
auf die geschichtliche Entwicklung der parallelen
Garbage Collectoren und auf die Methoden, die zum Beweis ihrer
Korrektheit benutzt wurden.
Im zweiten Teil wird eine Methodik zur Modellierung und
Verifikation paralleler Systeme vorgestellt, die High-Level Petrinetze mit
der von Chandy und Misra eingeführten UNITY-Logik kombiniert.
Wir beschreiben ein Netzkalkül sowie eine temporale Logik zur Formulierung
von Modelleigenschaften.
Darüberhinaus wird ein Konzept zur Komposition von Netzen durch
Vereinigung vorgestellt.
Im dritten Teil wird der parallele Garbage Collector von
Dijkstra et al. als Petrinetz modelliert. Grundlegende Eigenschaften
werden mit S-Invarianten nachgewiesen.
Im vierten und letzten Teil geben wir eine
formale Spezifikation des Collectors an,
anhand derer wir anschliessend die
Korrektheit unserer Modellierung beweisen.
Hans Stadtherr, 1997/09/16