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

Implementierung eines High-End-Model Checkers

Bearbeiter: offen
Aufgabensteller: Prof. Dr. Alexander Knapp
Betreuer: Moritz Hammer
Vorkenntnisse: Gute Kenntnisse oder die Bereitschaft zum Erlernen von C/C++ und systemnaher Programmierung unter Linux/POSIX

Ein expliziter Model Checker ist im wesentlichen ein effizienter Suchalgorithmus, der in z.T. extrem grossen Graphen nach Fehlerzuständen sucht. Da hierbei mitunter Terabytes an Daten bewegt werden, ist eine sehr effiziente Implementierung unabdingbar.

Inspiriert vom Erfolg von "Deep Fritz" im Tunier gegen den Schachweltmeister Kramnik soll der Einsatz von Multiprozessorsystemen für einen solchen Model Checker untersucht werden, da es hier unseres Wissens nach noch keine Ansätze gibt - zwar wird verteiltes Model Checking untersucht, aber dabei wird auf Rechnerclustern mit verteiltem Speicher gearbeitet. Der Einsatz von Multiprozessorrechnern mit shared memory verspricht andere Möglichkeiten der Optimierung.

Ausgehend von einer bestehenden Implementierung eines SPIN-kompatiblen Model Checkers (CMC) soll eine prototypische Implementierung eines solchen High-End-Model Checkers getestet werden. Hierzu ist eine gute Kenntnis der Programmiersprache C/C++ notwendig, die benötigten Mittel des POSIX-Standards sind einfach zu erlernen (vgl. diesen Artikel). Verschiedene Erweiterungen sind denkbar, wie eine Verallgemeinerung für allgemeine Hochperformanz-Berechnungen oder Einbeziehung spezialisierter Hardware (z.B. die Graphikkarte).