Paralleler und verteilter Aufbau des Zustandsraums im Model-Checker [mc]square

Motivation

Cluster auf Basis von normalen PC's sind mittlerweile weit verbreitet. Da die Methode des Model-Checkings sehr speicher- und rechenintensiv ist, macht es Sinn über eine Parallelisierung der in [mc]square verwendenten Algorithmen nachzudenken.

Ziel der Arbeit

Das Ziel dieser Arbeit ist es den Model-Checker [mc]square zu parallelisieren. Zu Beginn der Arbeit sollte eine Übersicht über parallele Algorithmen für CTL Model-Checking erstellt werden. Danach müssen die verschiedenen Ansätze miteinander verglichen werden und geprüft werden, welcher Ansatz am besten umzusetzen ist. Im Anschluss sollte eine Umsetzung in [mc]square erfolgen.

Studienrichtung

  • Informatik

Vorkenntnisse

  • Java
  • Programmieren von parallelen Programmen
  • ggf. Model-Checking

Student

Stefan Mau

Betreuer


RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland