Testautomatisierung

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 sequentieller 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, daß 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.

Aufgaben im WS2000/2001:

Aufgaben Serie WS2000-1 besteht aus der bereits behandelten Beispielspezifikation - die Aufgaben (3+1 optional) sind unten im CSP-Quelltext angefügt. Bearbeitung bis Montag 20.11.2000

Aufgaben aus früheren Semestern:

Aufgaben Serie 1

Aufgaben Serie 2

Aufgaben Serie 3 CSP-Channel Template (demoTA.csp) VVT-RT Demoversion (vvtDemo.tgz)

Aufgaben Serie 4

Aufgaben Serie 5 CSP-Channel Template (shell.csp) VVT-RT Demoversion für Aufgabe 2 (vvtShell.tgz)

Aufgaben Serie 6

Literatur:

CSP-Tutorium

Als formale Spezifikationssprache zur Beschreibung von Testspezifikationen wird eine Echtzeitvariante von CSP verwendet. Hierzu ist ein Tutorium (PDF-Format) verfügbar: Communicating Sequential Processes. Für den theoretischen Hintergrund (operationalle Semantik von Timed CSP) wird die Arbeit von Schneider (siehe unten) verwendet.

Theoretische Grundlagen

Das aktuelle Manuskript Testing Reactive Real-Time Systems wird derzeit noch im Bereich Echtzeit-Tests erweitert und modifiziert. Die Uebersicht in Part I und der sich auf Testen ohne Zeit beziehende Teil ist jedoch stabil und kann ohne schädliche Nebenwirkungen gelesen werden.

Die Veröffentlichung

    J. Peleska and M. Siegel: "Test Automation of Safety-Critical Reactive Systems." South African Computer Journal, 19:53-77 (1997).
ist im WWW über http://www.informatik.uni-bremen.de/~jp/jp_papers.html als Postscript-File erhältlich. Sie bildet die Grundlage der Vorlesung und enthält weitere Literaturangaben. Eine etwas ausführlichere Version mit verbesserten Beweisen findet sich im Kapitel 4 (Seite 102-140) meiner Habilitationsschrift, Formal Methods and the Development of Dependable Systems Diese Version der Beweise ist identisch mit der im Manuskript. Saetze und Beweise beziehen sich nur auf Testen ohne Zeit.

Warnung: Wer gerne den Stoff schon vor der Vorlesung vollständig verinnerlichen möchte, wird die obigen Arbeiten vielleicht nicht ganz trivial lesbar finden. Diese Einschätzung ändert sich dann garantiert schlagartig in der Vorlesung, wo - in gewohnter Weise - wieder unablässig motiviert, veranschaulicht, erläutert, ermuntert und notfalls auch getröstet wird.

Zur Vertiefung der Untimed-CSP Theorie sind die folgenden beiden Bücher zu empfehlen:

  • C.A.R. Hoare: "Communicating Sequential Processes", Prentice Hall (1985)
  • A.W. Roscoe: "The Theory and Practice of Concurrency", Prentice Hall (1998)

Die Timed-CSP Grundlagen basieren auf dem Paper:

  • S. Schneider: "An Operational Semantics for Timed CSP", Information and Computation 116, pp. 193-213 (1995)

[Uni [FB [TZI] [BISS]
emm@informatik.uni-bremen.de, letzte Änderung: 7. Januar 99