Dozent: Prof. Javier Esparza

Zeit und Ort:
Di 11:30-13:00 im Raum V38.02
Fr 11:30-13:00 (14-tägig) im Raum V38.02
Übung: Fr 14:00-15:30 (14-tägig) im Raum V38.03

Vorlesungstermine am Freitag:
2004: 22.10, 05.11, 19.11, 03.12, 17.12
2005: 21.01, 04.02, 11.02

Übungsseite

Hörerkreis: Studenten im Hauptstudium der Diplomstudiengänge Informatik und Softwaretechnik

Inhalt:
Entwickler im industriellen Bereich sind zwischen 50% und 70% der Zeit mit der Fehlererkennung und Fehlerkorrektur im neuen Code beschäftigt. Trotz dieses Aufwands ist die mangelnde Zuverlässigkeit vom Code eines der größten Probleme der Softwareindustrie. Wie Robert X. Cringely sagte: ``If the automobile had followed the same development cycle as the computer, a Rolls-Royce would today cost $100, get a million miles per gallon, and explode once a year, killing everyone inside''.

Diese Vorlesung vermittelt Grundprinzipien und Techniken für die Fehlererkennung und Fehlerkorrektur in Softwaresystemen. Zunächst werden Testing-Techniken präsentiert. Begriffe und Verfahren für systematisches Testen werden eingeführt: inspections, walkthroughs, control-flow coverage, data-flow coverage, black-box und white-box testing, test suites, conformance testing. Im zweiten Teil der Vorlesung werden Model-Checking-Verfahren für die automatische Programmverifikation behandelt. Zunächst wird die Problematik der Programmmodellierung erklärt und die temporale Logik CTL als formale Spezifikationssprache präsentiert. Anschließend werden enumerative und symbolische Model-Checking-Algorithmen beschrieben. Der dritte und letzte Teil der Vorlesung ist der Datenflussanalyse gewidmet. Die zugrundeliegende Theorie der Abstrakten Interpretation wird beschrieben, ebenso wie Anwendungen in den Bereichen Zuverlässigkeit und Code-Optimierung.

Skript:
Eine Folie pro Seite: PDF
Vier Folien pro Seite: PDF
Sechs Folien pro Seite: PDF

Die Folien von Dr. Karsten Schmidt über Berechnung von starkzusammenhängenden Komponenten in linearer Zeit (PDF-Datei) finden Sie hier (Seiten 12 bis 30)

Einige Dokumente:

• Informationen über den DO-178B Qualität-Standard für die Entwicklung von Software im Luftfahrtbereich (pdf)
• Spezifikation der Logical Link Control Schicht im ANSI/IEEE Standard 802.2 (Spezifikation von Protokollen für LAN-Netzwerke). In der Vorlesung wurden die Seiten 98-128 der PDF-Datei besprochen (pdf)
• Artikel erschienen am 19.6.2003 in The Economist
• Nasa's Mission Reliable. Artikel erschienen in IEEE Computer.
  

Literatur:

Glenford J. Myers:

Methodisches Testen von Programmen
R. Oldenbourg Verlag, 7. Auflage 2001
Englische Originalfassung: The Art of Software Testing
John Wiley and Sons, 1979

Gerard J. Holzmann:

Design and Validation of Communication Protocols
Prentice Hall Software Series, 1991.

Flemming Nielson, Hanne Riis Nielson und Chris Hankin:

Principles of Program Analysis
Springer Verlag, 1999.

Edmund C. Clarke, Orna Grumberg und Doron A. Peled:

Model Checking
MIT Press, 2000.

Doron A. Peled:

Software Reliability
Springer, 2001.