Testautomatisierung 2, Wintersemester 07/08

Inhalt dieser Seite

• Termine
• Überblick
• Veranstaltungsinhalte
• Übungszettel
• Leistungsnachweise
• Literatur

Termine

Überblick

Voraussetzung für die Veranstaltung ist die vorherige Teilnahme an Testautomatisierung I. Hilfreich, aber nicht zwingend notwendig, ist die vorherige Teilnahme an der Vorlesung Spezifikation eingebetteter Systeme.

Veranstaltungsinhalte

• Spezifikationsbasiertes Testen:
  • Automatische Testdatengenerierung und Testauswertung gegen Timed Automata und
  • Timed CSP
• Test hybrider Systeme, welche sowohl diskrete als auch analoge Messgrößen verarbeiten, automatisierter Test gegen Hybrid Statecharts
• Kennenlernen von Grundfunktionen und Entwurfsmerkmalen von Werkzeugen für die Testautomatisierung.
• Werkzeug-gestützter Entwurf und Durchführung von Tests für typische Beispiele von Echtzeit-Steuerungssystemen.

Übungszettel

Leistungsnachweise

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

Literatur

Allgemeines zum Testen

• R. Binder:,
  "Testing Object-Oriented Systems: Models, Patterns, and Tools",
  Addison-Wesley, 2000
  Testen objekt-orientierter Systeme.
• 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.

CSP

• 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.
• 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.
• C.A.R. Hoare:,
  "Communicating Sequential Processes",
  Prentice Hall, 1985
  Zur Vertiefung der Untimed-CSP Theorie.
• A.W. Roscoe:,
  "The Theory and Practice of Concurrency",
  Prentice Hall, 1998
  Zur Vertiefung der Untimed-CSP Theorie.
• 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.

Timed Automata

• Rajeev Alur, David L. Dill:
  A Theory of Timed Automata,
  Theoretical Computer Science, Volume 126, No 2, 1994
  DAS Paper zu Timed Automata.
• J.G. Springintveld, F.W. Vaandrager and P.R. D'Argenio:
  Testing timed automata,
  Theoretical Computer Science Volume 254, Issue 1-2, 6 March 2001
  pages 225-257.

Hybrid Automata

• Thomas A. Henzinger:
  The Theory of Hybrid Automata,
  Proceedings LICS 1996, IEEE Computer Society Press, 1996
  DAS Paper zu Hybrid Automata.
• Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine:
  The algorithmic analysis of hybrid systems,
  Theoretical Computer Science, Volume 138, 1994
  Nette Übersicht mit vielen Beispielen.
• R. Alur, T. Dang, J. Esposito, R. Fierro, Y. Hur, F. Ivancic, V. Kumar I. Lee, P. Mishra, G. Pappas, O. Sokolsky:
  Hierarchical Hybrid Modeling of Embedded Systems,
  Proceedings EMSOFT, 2001
  Hybrid und hierarchisch.
• Kirsten Berkenkötter, Stefan Bisanz, Ulrich Hannemann, Jan Peleska:
  HybridUML Profile for UML 2.0,
  SVERTS, workshop hold in conjunction with UML 2003, 2003
  Auch die Veranstalter spielen mit Hybrid Automata ;-)
• Kirsten Berkenkötter, Stefan Bisanz, Ulrich Hannemann, Jan Peleska:
  Executable HybridUML and Its Application to Train Control Systems,
  Springer LNCS 3147, 2004
  Unsere neuesten Erkenntnisse zu HybridUML

Testautomatisierung

• 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.
• 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.
• 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. vollständiges Tutorial [ps.gz]
• 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]
• 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]
• J. Peleska:,
  "Hardware/Software Integration Testing for the New Airbus Aircraft Families",
  TestCom 2002
• H. Löding, J. Peleska:
  "Symbolic and Abstract Interpretation for C/C++ Programs",
  Extended version of a submission to 3rd intl Workshop on Systems Software Verification (SSV08)
  [pdf]

Die W-Methode

• 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.
• 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.

Programmiersprache C

• B. Kernighan, D. Ritchie:,
  "The C Programming Language", 2nd Edition,
  Prentice-Hall, Upper Saddle River, NJ 07458, USA
  Das Standardwerk zur Programmiersprache C.
• 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.
• 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?"