Parallelisierung von ProB mit OSS

Das Thema ist bereits vergeben

Das am Lehrstuhl für Softwaretechnik und Programmiersprachen in Prolog entwickelte Werkzeug ProB dient dazu Systeme auf sicherheitskritische Eigenschaften hin zu überprüfen. Dazu wird der Zustandsraum durchlaufen und die Eigenschaften in jedem Zustand überprüft. Die Größe des Zustandsraums kann allerdings enorm gross sein, so daß das Überprüfen auf einem einzelnen Rechner unangemessen lange dauern kann. Parallelisierung der Anwendung und verteilte Ausführung kann hier Abhilfe schaffen. Die Parallelisierung ist verhältnismässig leicht zu bewerkstelligen (die Zustände stellen eine natürliche Grösse der Tasks dar), die Herausforderung ist die koordinierte verteilte Ausführung. Es bietet sich an den Zustandsraum in einem verteilten virtuellen Speicher (VVS) abzulegen auf den verteilte Rechner transparent zugreifen können. Wann einzelne Zustandsänderungen sichtbar werden hängt vom unterliegenden Konsistenzmodell ab. An der Abteilung Betriebssysteme wird ein Object Sharing Service (OSS) entwickelt der einen erweiterten VVS mit verschiedenen Konsistenzmodellen bereitstellt.

Im Rahmen der Arbeit soll die Repräsentation eines Zustandes im Speicher in C implementiert werden. Die Schnittstelle zwischen Sicstus Prolog und C ist gut benutzbar, es existieren bereits zwei in C geschriebene Erweiterungen für ProB. Außerdem soll mit Hilfe von OSS der Zustandsraum verteilt genutzt werden. Es sollen auch einfache verteilte Experimente durchgeführt werden.