Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > WiSe 2002/03 > Deutsch
English
 

Testautomatisierung, WiSe 2002/03
 
Vorlesung: Mo. 8-10 Uhr, GW2 B1700 Prof. Dr. Jan Peleska
Übung: Di. 13-15 Uhr, MZH 7210 Aliki Tsiolakis Achtung: Raumänderung!

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:

Ü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 CSP-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.

Literatur

  1. 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.
     
  2. 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.
     
  3. 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.
     
  4. C.A.R. Hoare "Communicating Sequential Processes", Prentice Hall, 1985.
    Zur Vertiefung der Untimed-CSP Theorie.
     
  5. A.W. Roscoe "The Theory and Practice of Concurrency", Prentice Hall, 1998.
    Zur Vertiefung der Untimed-CSP Theorie.
     
  6. 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.
     
  7. 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.
     
  8. 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 ...
    Auszug der relvanten Teile [ps.gz], vollständiges Tutorial [ps.gz]
     
  9. 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]
     
  10. 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]
     
  11. J. Peleska "Hardware/Software Integration Testing for the New Airbus Aircraft Families", TestCom 2002.
    [ps]
     
  12. 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
     
  13. 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.
     

Aufgabenblätter

Dieser Teil wird während des Semesters dynamisch erweitert.

Blatt 1: CSP-Spezifikationen zum Testen eines Engine Controller
[PS-2up], [PS], [PDF], [engine.csp], [ifm_sut.csp], [templ.csp],
Abgabe: 11. November 2002, vor dem Tutorium
   
Blatt 2: Test-Suite zum Testen des Engine Controllers
[PS-2up], [PS], [PDF], [engineController_TEMPLATE_ROBUSTNESS_v2.tgz]

Achtung: Das IFM des alten Templates (engineController_TEMPLATE.tgz) konnte noch nicht für Robustness-Tests verwendet werden! Deshalb bitte unbedingt das neue Template verwenden (eine schon für die Rechner in Ebene 0 compilierte Version von IFM und SUT findet sich hier). Die Änderungen können in der CSP-Definition des Interface-Moduls (ifm1/inc/ifm_1.csp) angesehen werden. Zusätzlich wurden die Makefiles sowie das config.rtt an die neue Struktur angepasst!

Hinweis: (1) Zusätzlich zu den Umgebungsvariablen für den RT-Tester (siehe die das User Manual) muss die Umgebungsvariable RTTTA auf das Verzeichnis gesetzt werden, in dem die Verzeichnisse ifm1, sut und test1 sind (z.B. engineController_TEMPLATE_ROBUSTNESS). (2) Auf den Linux-Rechnern in Ebene 0 muss auch noch der Pfad richtig gesetzt werden (wie im Tutorium berichtet), z.B. export PATH=/usr/bin:$PATH.
Abgabe: 03. Dezember 2002, vor dem Tutorium
   
Blatt 3: Testdokumentation des Engine Controller-Tests nach IEEE 829 (1998)
[PS], [PDF]
Abgabe: 17. Dezember 2002, vor dem Tutorium
   
Blatt 4: Checking-Algorithmen auf nicht-normalisierten Transitionsgraphen
[PS-2up], [PS], [PDF]
Abgabe: 28. Januar 2003, vor dem Tutorium
   

Veranstaltungsinhalte

Diese Liste wird während des Semesters fortlaufend erstellt und spiegelt am Ende des Semesters die in Vorlesung und Übung behandelten Themen wider.

  • Einbettung von Testen in Vorgehensmodelle
  • Klassifizierung von Testarten nach folgenden Kriterien
    • Integrationslevel (Unittests, Integrationstetss, Subsystemtests, Systemtests)
    • Umgebungsbedingungen (Test des Normalverhaltens, Test des Ausnahmeverhaltens)
    • Korrektheitseigenschaften (Funktionale Tests, Strukturtests)
    • Beobachtungstiefe (White-Box-Tests - Black-Box-Tests)
  • Test Case Specification, Test Case, Test Execution, Test Procedure, Test, Test Suite
  • Einführung in Timed-CSP zur Arbeit mit dem RT-Tester
  • Anforderungen an den Testling
    • Funktionale Anforderungen
    • Strukturelle Anforderungen
    • Nicht-funktionale Anforderungen (Zuverlässigkeit, Ergonomie, Last/Performance, Kompatibilität, Wartbarkeit, Dokumentation)
  • Deterministische Units vs. Nicht-Deterministische, Units mit/ohne Zeitbedingungen
  • Requirementsüberdeckung, Strukturüberdeckung (Statement Coverage, Branch Coverage, Path Coverage)
  • Test-Dokumentation nach IEEE 829 (1998): Standard for Software Test Documentation (Test Plan, Test Design Specification, Test Case Specification, Test Procedure Specification, Test Item Transmittal Report, Test Logs, Test Incident Reports, Test Summary Reports)
  • Spezifikationstechniken und Algorithmen für Testdatengenerierung und Auswertung
    • Test-Engine-Spezifikation: Generator (für SUT-Inputs) und Checker (zur Überprüfung von SUT-Outputs)
    • Back-to-back-Test (Implementierung eines Checkers auf Basis des Transitionsgraphen)
    • Hard Real-Time Algorithmus für automatisches Checking auf Basis
      • der Spezifikation des SUT
      • der Spezifikation der Systemumgebung
    • Normalisierung von Transitionsgraphen (zur Vermeidung von Backtracking):
      • Phase 1: Prä-Normalisierung
      • Phase 2: Reduktion
      • Literatur-Hinweis: [Roscoe94]
    • Checking auf nicht-normalisierten Transitionsgraphen in Soft-Real-Time (on-the-fly vs. offline)
    • Testdatengenerierung: Exhaustive Testing - Trace-Inklusion - White-Box-Testing - Zusicherungen in Trace-Logik oder Temporaler Logik - Failure-Inklusion
      • Coverage für Reqirements
      • Coverage für Trace-Inklusion
      • Depth-First-Search (DFS) zum Aufsuchen aller Knoten und Kanten eines Transitionsgraphen
      • W-Method (Tutorium, Literatur-Hinweis: [Sadeghipour98])
      • Timed Trace Inclusion
    • Überdeckung
      1. aller Pfade
      2. aller States des SUT
      3. aller Robustheitssituationen
      4. im Zeitbereich [0,t)
  • CSP und Timed-CSP: Einführung in die Operationelle Semantik und Denotationelle Semantik
  • ...

Added Value

Eine kleine Sammlung von nützlichen Links und Hinweisen, die während des Semesters hier zur Verfügung gestellt werden.

 
   
Autor: jp 		 
  AG Betriebssysteme, Verteilte Systeme 
Zuletzt geändert am: 2. November 2022   Impressum