Dozent:	Prof. Javier Esparza
Ankündigungen:	Die Musterlösung zur Klausur ist jetzt auf der Übungsseite verlinkt.
Zeit und Ort:	Di 11:30-13:00 im Raum V38.02
	Dienstagstermine 05: 18.10, 8.11, 15.11, 22.11, 29.11, 6.12, 13.12, 20.12
	Fr 11:30-13:00 (14-tägig) im Raum V38.02
	Freitagstermine 05: 28.10, 4.11, 11.11, 18.11, 2.12, 16.12
	Freitagstermine 06: 20.01, 03.02, 17.02 (geändert).
Übungen:	Fr 14:00-15:30 (14-tägig) im Raum V38.03
	Ü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:	Folien: [PDF]
	Folien zur Minimierung von DMMs [PDF]
	Die Folien von Dr. Karsten Schmidt über die Berechnung der SCCs in Linearzeit (Tarjan-Algorithmus) finden Sie [hier] (Seiten 12 bis 30).
	Folien von WS0405: [PDF]
Einige Dokumente:	Informationen über den DO-178B Qualität-Standard für die Entwicklung von Software im Luftfahrtbereich [PDF]
	Wikipedia-Eintrag über berühmte Computer-Bugs
	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.