Modulbezeichnung | Software-Analyse - Software-Qualität |
ggf. Kürzel | 5840 |
Studiensemester | 1.-3. (Master Inf.) |
Modulverantwortlicher | Beyer |
Dozent | Beyer |
Sprache | englisch |
Zuordnung zum Curriculum |
|
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. |