Modul 5840 -- Software-Analyse - Software-Qualität


Modulbezeichnung Software-Analyse - Software-Qualität
ggf. Kürzel 5840
Studiensemester 1.-3. (Master Inf.)
Modulverantwortlicher Beyer
Dozent Beyer
Sprache englisch
Zuordnung zum Curriculum WF MA Inf. SP ProgSoft; WPF MA IT-Sicherheit
Lehrform/SWS 2 V + 1 Ü + 2 Projekt
Arbeitsaufwand 75 h Präsenz (V + Ü) + 30 h Übungsaufgaben bearbeiten + 30 h  Nachbearbeitung des Vorlesungsstoffs und Prüfungsvorbereitung + 75 Std. Projektarbeit
Kreditpunkte 7
Voraussetzungen nach Prüfungsordnung keine
Empfohlene Voraussetzungen 5300 - Software Engineering, 5102 - Programmierung I
Angestrebte Lernergebnisse Kenntnisse:
Die Studierenden erlernen grundlegende Prinzipien und erwerben Kenntnisse über moderne Techniken für die Bewertung und Verbesserung der Qualität von Softwaresystemen.

Fähigkeiten:
In den Übungen vertiefen die Studenten das in der Vorlesung behandelte Wissen bei der Lösung von Übungsaufgaben. Im Semesterprojekt entwerfen und implementieren die Studenten eigene Komponenten für ein Software-Analysewerkzeug (Struktur und/oder Verhalten).

Kompetenzen:
Die Studenten können formale Techniken als praktisches Mittel zur Gestaltung und zur Analyse von Softwaresystemen in der industriellen Praxis einsetzen. Die Anwendungen konzentrieren sich auf die Analyse von Software-Graphen und Quelltext.
Inhalt Die Vorlesung behandelt wichtige Prinzipien und Verfahren der Softwareanalyse, insbesondere Datenflussanalyse, Software Model Checking, Testen, Strukturanalyse. Die Studenten lernen formale Techniken als praktisches Mittel zur Analyse von Softwaresystemen kennen. Hervorgehoben wird Werkzeugunterstuetzung. Die Anwendungen  konzentrieren sich auf die Analyse von Quelltext. Im Semesterprojekt entwerfen und implementieren die Studenten eigene Komponenten fuer ein Software-Analysewerkzeug.

Kurzuebersicht zur Vorlesung:

    * Programanalyse, Datenflussanalyse
    * Abstract Domains und Abstract Interpretation
    * Software Model Checking, gegenbeispielbasierte Abstraktionsverfeinerung
    * Generierung von Programminvarianten
    * Testen, Testfall-Generierung, geführtes Zufallstesten
    * Analyse der Struktur von großen Softwaresystemen
    * Relationale Programmierung
    * Software-Visualisierung
    * Schnittstellen und komponentenbasierter Entwurf, Webservice-Schnittstellen
    * Verifikation endlicher Automaten
    * Datenstrukturen für die Repräsentierung von endlichen Zustandsmengen
    * Verifikation unendlicher Zustandsmengen, Echtzeitsysteme
    * Datenstrukturen für die Repräsentation unendlicher Zustandsmengen
    * Anwendungen von Therembeweisern

Studien-/Prüfungsleistungen Mündliche Prüfung (30 min) und erfolgreiche Durchführung des Semesterprojektes, letzteres nachgewiesen durch praktische Leistung bei der selbständigen Erarbeitung, Implementierung und Präsentation der eigenen Softwarekomponente, sowie durch die Abgabe des Projektberichtes mit Erklärung der Konzepte und der Implementierung. Die Gesamt-Note setzt sich zu je 50 % aus der Teil-Note für die Prüfung und der Teil-Note für das Semesterprojekt zusammen.
Medienformen Tafel + Projektor
Literatur F. Nielson, H. R. Nielson, C. Hankin. Principles of Program Analysis. Springer, 2005.
E. M. Clarke, O. Grumberg and D. Peled. Model Checking. MIT Press, 2000.
G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.