Eine der wichtigsten Qualitätssicherungsmaßnahmen für Software ist die Durchführung von Tests. Die steigende Komplexität moderner Softwaresysteme erfordert eine immer größere Anzahl von Tests um eine verläßliche Garantie für das korrekte und sichere Funktionieren von Software geben zu können. Die große Anzahl macht es unwirtschaftlich oder gar unmöglich Testfolgen manuell zu erstellen. Ein weiteres Problem ist die Auswahl der Tests. Wann kann man sagen, den größten Teil möglicher Fehlerquellen abgedeckt zu haben? Als eine Lösung für beide Probleme wurde das modellbasierte Testen eingeführt. Man geht hier von einem Modell der zu erstellenden Software aus und zeigt zunachst mit größtenteils vollautomatischen Verfahren, daß das Modell die gewünschten Eigenschaften hat. Diese Verfahren nennt man Modellprüfungsverfahren (im Englischen model checking). Durch eine sorgfältige Analyse des Modellprüfungsverfahrens kann man nun feststellen, welche einzelnen Eigenschaften für einen positiven Ausgang des Verfahren notwendig oder sogar entscheidend waren. In einem zweiten Schritt werden nun Tests generiert, die überprüfen, ob diese Eigenschaften nicht nur im Modell vorliegen, sondern auch für dessen Implementierung zutreffen. Für die Durchführung von Tests kann man zwei prinzipiell unterschiedliche Vorgehensweisen unterscheiden. Zum einen das offline Verfahren. Hier wird die Folge der geplanten Tests erstellt und dann werden alle Tests durchgeführt. Die zweite Möglichkeit stellt das on-the-fly Verfahren dar. Hier wird die Testgenerierung und die Durchführung von Tests miteinander verzahnt. Abhängig von dem Ergebnis eines Testlaufs werden weitere Tests erzeugt oder nicht. Ein solches Vorgehen ist insbesondere für nichtdeterministische Systeme unerläßlich. Ein typisches Beispiel für nichtdeterministische Systeme, mit denen man hier rechnen muß, sind Systeme die von der Kommunikation über Netzwerke abhängen. Hier kann im allgemeinen nicht garantiert werden wann und in welche Reihenfolge Nachrichten eintreffen. Das abgeschlossene Projekt trägt an zwei Stellen zum Fortschritt im modellbasierten Testen bei. Ersten wurden effizientere Algorithmen für Modellprüfungsverfahren vorgeschlagen, theoretisch analysiert, implementiert und ausgiebig getestet. Zweites wurde ein neues Verfahren zur automatischen Testfolgengenerierung vorgeschlagen und prototypisch seine Machbarkeit und seine Vorteile gegenüber bisherigen Verfahren demonstriert. Das Verfahren beruht auf einer geschickten Kombination von offline und on-the-fly Verfahren.