Integration von Modellprüfung und Automatischer Testgenerierung

• Antragsteller: Professor Dr. Peter H. Schmitt
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2009 bis 2013
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 137421300

• Erstellungsjahr: 2014

Zusammenfassung der Projektergebnisse

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.

Projektbezogene Publikationen (Auswahl)

• Improving non-progress cycle checks. Corina S. Pasareanu, editor. Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings, volume 5578 of Lecture Notes in Computer Science. Springer, 2009, pages 50–67
  David Faragó and Peter H. Schmitt
  
• Correctness of sensor network applications by software bounded model checking. In Stefan Kowalewski and Marco Roveri, editors. Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. Proceedings, volume 6371 of Lecture Notes in Computer Science. Springer, 2010, pages 115– 131
  Frank Werner and David Faragó
  
• Coverage criteria for nondeterministic systems. Testing Experience. The Magazine for Professional Testers, pages 104–106, September 2010
  David Faragó
  
• Improved underspecification for model-based testing in agile development. In Stefan Gruner and Bernhard Rumpe, editors. FM+AM 2010 - Second International Workshop on Formal Methods and Agile Methods, 17 September 2010, Pisa (Italy), volume 179 of LNI. GI, 2010., pages 63–78
  David Faragó
  
• Model-based testing in agile software development. Softwaretechnik-Trends, 30(3), 2010
  David Faragó
  
• Modellbasiertes Testen: Hype oder Realität? OBJEKTspektrum, (06):59–65, 2011
  Stephan Weißleder, Baris Güdali, Michael Mlynarski, Arne-Michael Törsel, David Faragó, Florian Prester, and Mario Winter
  
• Nondeterministic coverage metrics as key performance indicator for model- and value-based testing. Softwaretechnik-Trends, 31(1), 2011
  David Faragó
  
• Improved on-the-fly livelock detection. In Guillaume Brat, Neha Rungta, and Arnaud Venet, editors. NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, volume 7871 of Lecture Notes in Computer Science. Springer, 2013, pages 32–47
  Alfons Laarman and David Faragó
  
• Wirtschaftlichkeitsberechnung für MBT: Wann sich modellbasiertes Testen lohnt. OBJEKTspektrum, (04), 2013
  David Faragó, Stephan Weißleder, Baris Güdali, Michael Mlynarski, Arne-Michael Törsel, and Christian Brandes