Ludwig-Maximilians-Universität München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

Fortgeschrittenenpraktikum

Model Checking eines Rekonfigurationsprotokolls

Inhalt

Im Rahmen des JComp-Komponenten-Frameworks wurde ein Protokoll implementiert, dass die Rekonfiguration nebenläufiger Komponenten realisiert. Man kann sich dies so vorstellen, als wenn bei kommunizierenden Computern ein Computer durch einen anderen ersetzt wird, ohne daß die anderen beteiligten Computer den Unterschied bemerken.

Da dieses Protokoll in einem extrem nebenläufigen Umfeld implementiert ist, ist die Korrektheit mit Tests nur sehr schwer zu überpräfen, und etwaige Fehler sind nur schwer auf ihre Ursache zurückführbar. Mittels Model Checking einer abstrahierten Modellierung des Protokolls könnte hier Klarheit geschaffen werden, ob das Protokoll einige Eigenschaften erfüllt, von denen die Transparenz für andere Komponenten die wichtigste ist. Da die Implementierung vorliegt, könnte auch versucht werden, aus den Java-Sourcen ein geeignetes Modell zu extrahieren oder entsprechende Tools zu testen.

Ziel des FoPras ist es, die Korrektheit des Rekonfigurations-Protokolls per Model Checking glaubhaft zu machen und Erfahrung ueber die notwendigen Abstraktionsschritte zu sammeln und zu dokumentieren.

Bearbeiter: offen
Aufgabensteller: Prof. Dr. Knapp
Betreuer: Moritz Hammer,