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.

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.

• Informatik

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

Stefan Mau

• Dr.rer.nat. Bastian Schlich