1 1  Einleitung Beim   Entwurf   und   bei   der   Implementierung v on   Software   spielen   das   Testen   und   die Verifikation,   sprich die   Überprüfung,   ob   das   Verhalten   der   Software   der   Spezifikation folgt,   eine   große   Rolle.   Besonders   bei   sicherheitskritischen   Programmen,   wie   Software für die Luft- und Raumfahrt oder für Kernkraftwerke,     können     Fehler     in     der Implementierung   schwerwiegende   Folgen   haben.   Beim   Testen    wird   das   Verhalten   des Gesamtsystems     oder eines     Teilesystems     aufgrund     ausgewählter     Eingabevariablen     in bestimmten Umgebungen getestet. Nach den Testdurchläufen werden dann die Resultate    mit    den    gewünschten   Ergebnissen   verglichen. Jedoch   sind   die   Wertebereich für   die   Eingabevariablen   meist   sehr   groß   bzw.   unendlich,   was   zur   Folge   hat,   dass   die generierten   Testfälle   nie   das   gesamte   Verhalten   des   Systems   abdecken   können.   Auch bei    parallelen    Systemen    sind    dem    Testen    Grenzen    gesetzt.    Dahingegen    basiert    die Verifikation   auf analytischen    Verfahren   zum   Überprüfen   des   Verhaltens   der   Software. Diese    sind    zwar    aufwendiger,    dafür    aber    effektiver.    Deshalb    wurde besonders    das Verfahren d es   Model-Checking,   bei   dem   automatisiert   das   Verhalten   der   Programme mit der Spezifikation verglichen wird, in den letzten Jahren konsequent weiterentwickelt.   Während   die   ersten   „Model-Checker“   sich   noch   auf   das   Prüfen   der Funktion von Hardware und einfachen Kommunikationsprotokollen beschränkten, können  heute  sogar  schon  komplexe    Programme  überprüft  werden.  Das  „NASA  Aimes Research  Center“  hat  für  Java  einen  Model-Checker  mit  dem  Namen  „Java  Path  Finder“ (JPF)   entwickelt,   der   auf   die   Objekt-Orientierung      und   Multi-Threading-Fähigkeit  dieser Programmiersprache   zugeschnitten   ist.   Dieser   JPF   und   dessen   Weiterentwicklung   sollen der Hauptgegenstand dieser Arbeit sein. Zuerst   wird   im   zweiten   Abschnitt   dieser   Arbeit   auf   die   Herausforderungen   eingegangen, die     Java     an     das     Model     Checking     stellt.     Danach     wird im     dritten     Abschnitt die Funktionsweise   des   Java   Path   Finders   und   dessen   Weiterentwicklungen   aufgezeigt.   Der vierte   Abschnitt   zeigt   ein   Beispiel,   welches  aus  realen  Forschungen  des  „NASA  Aimes Research   Centers“   hervorgegangen   ist.   Der   letzte   Abschnitt   ist   eine   Zusammenfassung und ein kurzer Ausblick auf das, was die Forscher in Zukunft machen wollen.