Lehre: Softwarezuverlässigkeit - Fachbereich Elektrotechnik und Informatik

Softwarezuverlässigkeit

Gegenstand der Lehrveranstaltung ist eine Einführung in grundlegende Techniken der Software-Zuverlässigkeit: Verfahren, um Laufzeitfehler und funktionale Fehler (Verletzung der Anforderungen) aufzufinden bzw. zu vermeiden.

Die zunehmende Komplexität und der allgegenwärtige Einsatz von Softwaresystemen rückt das Problem der Zuverlässigkeit solcher Systeme zunehmend in den Fokus. Wie können wir sicherstellen, dass Softwaresysteme mit hoher Wahrscheinlichkeit ihre Funktion erfüllen? In diesem Modul lernen Studierende sowohl klassische Verfahren für die Sicherstellung der Software-Zuverlässigkeit, als auch Kriterien für die Beurteilung der Qualität einer gegebenen Software in Hinblick auf ihre Zuverlässigkeit kennen. Neben verschiedenen Softwaretestverfahren und Testabdeckungskriterien wird auch die statische Code-Analyse behandelt und ein Einblick in die formale Softwareverifikation gegeben. Ein besonderer Fokus wird auf skalierbare Verfahren gelegt, welche Softwaretests mit statischer Code-Analyse kombinieren.

Zielgruppe

Studierende des Bachelorstudiengangs Informatik im 5. Semester

Form

Vorlesung (2 SWS) und Praktikum (2 SWS)

Inhalte

Klassische Softwaretestverfahren
- Äquivalenzklassen und Grenzwertanalyse
- Codeüberdeckungsmaße
Systematisches Testen & Model Checking
- Durchsuchung des Zustandsraums
- Abstraktion: Modellierung
- Modell und Implementierung
- Praktikum: TLA+
Fuzzing & Symbolic Execution
- Generierung von Testeingaben für eine hohe Codeüberdeckung mittels
- Vor- und Nachteile beider Ansätze
- Praktika: AFL++, Z3 SMT Solver, IntelliTest
Programmverifikation
- Korrektheits- und Vollständigkeitsbeweise
- Schleifeninvarianten
- Praktikum: Dafny

Organisatorisches

Zielgruppe	Bachelor Informatik, Bachelor Informatik dual
Turnus	jedes Wintersemester
Lehrformen	Vorlesung (2 SWS), Praktikum (2 SWS)
Leistungspunkte	5
Voraussetzungen	Die Prüfungen in den folgenden Modulen müssen bestanden sein: - Einführung in die Informatik - Einführung in die objektorientierte Programmierung - Mathematik I - Mathematik II - Theoretische Informatik Die Module des dritten und vierten Studiensemesters sollten erfolgreich absolviert sein.
Voraussetzungen zur Prüfungsteilnahme	Erfolgreiche Teilnahme am Praktikum
Prüfungsform	Das Modul wird regelmäßig abgeschlossen durch eine schriftliche oder mündliche Prüfung. Die im aktuellen Semester geforderte Prüfungsleistung entnehmen Sie bitte der Prüfungsliste des Fachbereichs Elektrotechnik und Informatik, die spätestens vor Beginn der Vorlesungszeit des Semesters veröffentlicht wird.

Literatur

Kapitel 1: Klassische Softwaretestverfahren:

Kleuker, Qualitätssicherung durch Softwaretests
- Kapitel 4 und 5
Aniche, Effective Software Testing
- Kapitel 2 und 3

Kapitel 2: Systematisches Testen & Model Checking

Dokumentation des JavaPathFinders
- What is JPF
- Testing vs. Model Checking
Kleuker, Formale Modelle der Softwareentwicklung
- Kapitel 2
Dokumentation TLA+
- TLA+ Website

Kapitel 3: Fuzzing & Symbolic Execution

The Fuzzing Book

Kapitel 4: Programmverifikation

Kleuker, Formale Modelle der Softwareentwicklung
- Kapitel 5
K. Leino, Program Proofs