Entkopplung einer Komponente in ProB
Umfang
Dieses Thema kann als Bachelorarbeit bearbeitet werden.
Empfohlene Vorkenntnisse
- gute C oder C++ Kenntnisse
- hilfreich: Prolog Kenntnisse
Problem
In ProB (Prolog) haben wir als Backend, um Prädikate zu lösen, den Z3 Solver (C/C++) eingebunden. In der Vergangenheit hatten wir aber einige Probleme damit, wie etwa, dass langsam Speicher leckt oder dass Segmentation Faults auftreten. Daher wäre es sinnvoll, Z3 in einem separaten Prozess auszuführen. Dann könnte man beispielsweise auch mehrere Instanzen starten und parallel verschiedene Prädikate lösen.
Als Technologie zur Kommunikation zwischen zwei Prozessen haben wir gute Erfahrungen mit der ZeroMQ-Bibliothek gemacht. Ihre Aufgabe in dieser Arbeit wäre daher, eine Brücke mittels ZeroMQ zwischen dem C-Interface, in dem derzeit die Prädikate zusammengebaut und gelöst werden, und einem neuen Prozess, der Z3 wrappt und die Calls weitergibt, zu schlagen.
Minimalanforderungen
- Trennung von ProB und Z3 mittels ZeroMQ
- Evaluation des Performance-Overheads
Erweiterungen
- ggf. alternative Lösungsansätze
Kontakt
Philipp KörnerRaum 25.12.02.56
p.koerner@hhu.de