Abgeschlossen am 23.10.14 von Andreas Wrasmann.

Synchronisationskonzepte für Anwendungsprogramme, Model Checking, SAT

In den Modulen Betriebssysteme 1"  und Betriebssysteme 2 werden Synchronisationsprobleme behandelt, die mit verschiedenen Synchronisationskonzepten (Semaphore, Monitore, Rendezvous-Konzept, Nachrichten) gelöst werden sollen. Der Beweis, dass solch ein Synchronisationsproblem korrekt gelöst wurde, ist in der Regel sehr schwierig und bedarf eines mathematischen Beweises. Der Gegenbeweis, dass eine Lösung fehlerhaft ist, ist dagegen meist einfacher, da die Konstruktion eines einzigen Gegenbeispiels genügt. Nichtdestotrotz ist dies mitunter sehr zeitaufwaendig und mühsam, insbesondere im Übungsbetrieb, da dort sehr viele verschiedene potentielle Lösungen generiert werden und sich die Tutoren erst in jeden Lösungsversuch hineindenken müssen. Die Erfahrungen der letzten Jahre haben gezeigt, dass (leider) die meisten Lösungsversuche fehlerhaft sind und dass oftmals man einen Ablauf konstruieren kann, bei dem das Synchronisationsproblem nicht korrekt gelöst wird.

Es soll untersucht werden, in wie weit sich Gegenbeispiel wie oben skizziert automatisch generieren lassen, um die Fehlerhaftigkeit zu zeigen. Als Basis sollen einfache, vermeintliche Lösungen, spezifiziert in der von der Abteilung und in den Modulen genutzten Systemprogrammiersprache dienen.

• Prof. Dr.-Ing. Oliver Theel
• Dipl.-Inform. Eike Möhlmann