18 5  Zusammenfassung Ein Ansatz, das Model-Checking auf Software-Systemen anzuwenden, die in komplexen     Programmiersprachen (wie     Java)    implementiert    sind,    ist    der    Java    Path Finder.    Die    Funktionsweise    des    JPFs    basiert    grundlegend    auf der    Abstraktion    der Programme.   Die   abstrakten   Programme   konzentrieren   sich   dabei   nur   auf   die   relevanten Eigenschaften des Verhaltens der Software.   Diese    Arbeit    gibt    dazu    eine    kurze    Einführung    in    das    Thema.    Zuerst    werden    die Anforderungen,    die    komplexe    Programmiersprachen    an    das    Model-Checking    stellen, erörtert.  Dann  werden  die  Techniken  beschrieben,  die  der  JPF  verwendet,  um  Daten  zu abstrahieren,     um     Fehler     aufzudecken     und     um     Pfade     zu     generieren,     die bei     der Ausführung   des   Programms   zu   diesen   Fehlern   führen.   Zum   Abschluss   wird   ein   kurzes Beispiel  dargestellt,  welches  zeigt,  dass  die  Techniken  des  JPFs  in  der  Praxis  angewandt werden,    und    die    Weiterentwicklung    von    Programmen    zum    Model-Checking    in    der Forschung ein ernst genommenes Thema ist.