Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > WiSe 2013/14 > Deutsch
English
 

Grundlagen von Test und Verifikation, Wintersemester 2013/2014

 


Auf dieser Seite werden weiterführende Informationen zur Lehrveranstaltung sowie die jeweiligen Aufgabenzettel bereitgestellt. Wir bemühen uns, die Seite so aktuell wie möglich zu halten.


Informationen:


Termine

Do. 10-14 Uhr, MZH 1090, Beginn am 24.10.2013, Prof. Dr. Jan Peleska, Elena Gorbachuk


Überblick

Auf dem Gebiet der Testautomatisierung sind in den letzten Jahren erhebliche Fortschritte erzielt worden, so daß die zur Zeit in vielen Softwarehäusern noch praktizierte intuitiv-heuristische Vorgehensweise nicht mehr als "Stand der Kunst" bezeichnet werden kann. Die Problemstellung wird unterteilt in den Test sequenzieller Komponenten, bei denen Datenstrukturen und darauf operierende Algorithmen im Vordergrund stehen und in den Test reaktiver Systeme, bei denen Parallelität, Synchronisation, Timing und Steuerungsentscheidungen die größte Bedeutung haben.

In dieser Vorlesung steht der Test eingebetteter reaktiver Systeme (Hardware und Software) im Mittelpunkt. Typische "Testlinge" sind Steuerkomponenten für Stellwerke, Überwachungskomponenten für ausfallsichere Systeme und ähnliche - meist sicherheitsrelevante - Anwendungen. Wir stellen die theoretischen Grundlagen dar, welche die automatische Generierung, Durchführung und Auswertung von Tests gegen formale-Spezifikationen ermöglichen. Dabei wird gezeigt, wie diese theoretischen Ergebnisse in Werkzeugen implementiert werden. Im praktischen Teil wird die Anwendung der Theorie für den Test reaktiver Systeme demonstriert.

Aufgrund der zunehmenden Kritikalität vieler eingebetteter Systeme und der hierdurch drastisch anwachsenden Kosten für Validation, Verifikation und Test ist das Gebiet Testautomatisierung ein echter "Zukunftsmarkt". Die vorgestellten Grundlagen und praktischen Resultate sind bereits in Industrieanwendungen, u.a. mit der DASA (heute ASTRIUM), EADS Airbus, OHB, Siemens und mit South African Railways, mit sehr gutem Erfolg erprobt worden. Fast schon überflüssig zu sagen, dass unsere Bremer Arbeitsgruppe auf diesem Gebiet "Leading Edge Technology" erarbeitet hat ;-). Neben der praktischen Relevanz gibt es hier auch noch ein sehr weites Feld für Diplomarbeiten und Dissertationen.


Material zur Vorlesung


Veranstaltungsinhalte

Dieser Teil wird während des Semesters dynamisch erweitert.


Übungszettel


Leistungsnachweise

Einen benoteten Leistungsnachweis erhaltet Ihr bei erfolgreich erbrachter Prüfungsleistung:

  • Entweder durch erfolgreiches Bearbeiten von Übungsaufgaben inkl. bestandenem Fachgespräch,
  • oder durch eine bestandene mündliche Prüfung (alias Modulprüfung).


Literatur

  1. R. Binder "Testing Object-Oriented Systems: Models, Patterns, and Tools", Addison-Wesley, 2000
     
  2. A. Spillner, T. Linz "Basiswissen Softwaretest: Aus- und Weiterbildung zum Certified-Tester", dpunkt-Verlag, 2003.
    Das Basiswissen für diese Lehrveranstaltung wird in diesem Buch sehr gut erläutert.
     
  3. CSP-Tutorium
    Als formale Spezifikationssprache zur Beschreibung von Testspezifikationen wird eine Echtzeitvariante von CSP verwendet, dass in dem zur Verfügung gestellten CSP-Tutorium vorgestellt wird.
    [PDF]
    Für den theoretischen Hintergrund (operationelle Semantik) sei auf die Arbeit von Schneider verwiesen.
     
  4. S. Schneider "An Operational Semantics for Timed CSP", Information and Computation 116, pp. 193-213, 1995.
    Die Timed-CSP Grundlagen der Vorlesung basieren auf diesem Paper.
     
  5. C.A.R. Hoare "Communicating Sequential Processes", Prentice Hall, 1985.
    Zur Vertiefung der Untimed-CSP Theorie.
     
  6. A.W. Roscoe "The Theory and Practice of Concurrency", Prentice Hall, 1998.
    Zur Vertiefung der Untimed-CSP Theorie.
     
  7. J. Peleska und M.Siegel "Test Automation of Safety-Critical Reactive Systems", South African Computer Journal, No. 19, pp. 53-77, 1997.
    [Abstract], [ps.gz]
    Dieses Paper bildet die Grundlage der Vorlesung und enthält weitere Literaturangaben. Eine etwas ausführlichere Version mit verbesserten Beweisen findet sich in der Habilitationsschrift von Jan Peleska.
     
  8. J. Peleska"Formal Methods and the Development of Dependable Systems", Habilitationsschrift, Bericht Nr. 9612, Dezember 1996, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel, 1997.
    [ps.gz]
    Die Version der Beweise ist identisch mit dem Tutorial FTRTFT '98. Sätze und Beweise beziehen sich nur auf Testen ohne Zeit.
     
  9. J. Peleska, P. Amthor, S. Dick, O. Meyer, M. Siegel, C. Zahlten "Testing Reactive Real-Time Systems", Tutorial, held at the FTRTFT '98. Danmark Technical University, Lyngby, 1998.
    Für die Vorlesung ist vor allem die Übersich in Part I und der sich auf Testen ohne Zeit beziehende Teil relevant. Der Bereich Echtzeit-Tests ...
    vollständiges Tutorial [ps.gz]
     
  10. J. Peleska "Formal Methods for Test Automation - Hard Real-Time Testing of Controllers for the Airbus Aircraft Family", Invited Talk. Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology (IDPT2002), Pasadena, California, June 23-28, 2002.
    [ps]
     
  11. A.E. Haxthausen, J. Peleska "A domain specific language for railway control systems", Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology, IDPT2002, Pasadena, California, June 23-28, 2002.
    [ps]
     
  12. J. Peleska "Hardware/Software Integration Testing for the New Airbus Aircraft Families", TestCom 2002.
     
  13. A. W. Roscoe "Model-checking CSP", in "A Classical Mind: Essays in Honour of C.A.R. Hoare", edited by A. W. Roscoe, Prentice-Hall, 1994,
    Beschreibung des Normalisierungsalgorithmus
     
  14. Tsun S. Chow "Testing Software Design Modeled by Finite-State Machines", IEEE Transactions on Software Engineering, SE-4(3), pp. 178-186, März 1978.
    Originalartikel zur W-Method.
     
  15. S. Sadeghipour "Testing Cyclic Software Components on the Basis of Formal Specifications", Verlag Dr. Kovac, Hamburg 1998, Dissertation an der TU Berlin (1998)
    Beschreibung der W-Method zur Generierung von Test-Input-Traces.
     
  16. B. Kernighan, D. Ritchie "The C Programming Language", 2nd Edition, Prentice-Hall, Upper Saddle River, NJ 07458, USA
    Das Standardwerk zur Programmiersprache C.
     
  17. T. Love "ANSI C for Programmers on UNIX Systems", http://www.eng.cam.ac.uk/help/tpl/languages/C/teaching_C/teaching_C.html
    ANSI C Tutorial
     
  18. S. Summit "comp.lang.c Frequently Asked Questions", http://www.eskimo.com/~scs/C-faq/top.html
    FAQ der Nachrichtengruppe comp.lang.c, s. insbesondere Frage 18.9: "Are there any C tutorials or other resources on the net?"
     


Testwerkzeug RT-Tester

Für die praktische Umsetzung von Tests verwenden wir das Testwerkzeug RT-Tester.


 
   
Autor: jp
 
  AG Betriebssysteme, Verteilte Systeme 
Zuletzt geändert am: 16. Oktober 2015   Impressum