Softwarequalität 1 ist keine zwingende Voraussetzung für diese Vorlesung!
Dozent: Prof. Dr. Ina Schaefer
Betreuer: Tabea Bordis, M.Sc.
Modulnummer: INF-SSE-38
Veranstaltungsnummer: INF-SSE-050 / INF-SSE-051
Die Vorlesungsmaterialien und die Lösungen der Übungsaufgaben werden wöchentlich an folgenden Terminen besprochen:
Formale Methoden bezeichnen Methoden für den Systementwurf oder die Systemanalyse und Implementierungstechniken, die mit mathematischer Exaktheit beschrieben werden. Das Ziel ist es, Systeme zu konstruieren, die sich mit hoher Zuverlässigkeit gemäß ihrer Spezifikation verhalten. Diese Lehrveranstaltung führt theoretisch und praktisch die beiden wichtigsten Arten der formalen Methoden für die Analyse von Programmen ein: Software Model Checking und deduktive Verifikation.
Die Vorlesung beschäftigt sich mit folgenden Themen:
Die Veranstaltung Softwarequalität 2 findet in diesem Semester online statt. Die Vorlesungs- und Übungsunterlagen werden ausschließlich im Stud.IP hochgeladen. Bitte melden Sie sich daher frühzeitig für die Vorlesung und die Übung Softwarequalität 2 im Stud.IP an. Das bereitgestellte Material darf nicht an Dritte weitergeben oder frei veröffentlicht werden.
Für die Vorlesung werden Foliensätze und Videos hochgeladen.
Für die Übung werden Aufgabenzettel hochgeladen, die von den Studierenden bearbeitet werden können. Dabei wird es sowohl Aufgaben geben, die auf dem Papier zu lösen sind, als auch Aufgaben, die am Computer gelöst werden müssen. Falls die Benutzung von Tools erforderlich ist, befinden sich die Informationen dazu auf dem Aufgabenzettel.
Sowohl für die Vorlesung als auch die Übung wird es an den oben genannten Terminen in der jeweiligen StudIP Veranstaltung eine Live-Session geben, in der Fragen gestellt werden können und im Falle der Übung auch die Lösungen der einzelnen Aufgabenblätter besprochen werden. Dabei wünschen wir uns rege Beteiligung seitens der Kursteilnehmer. Wir dürfen diese Live-Sessions aus rechtlichen Gründen nicht aufzeichnen und danach online stellen!
Die Prüfungsleistung wird in Form einer mündlichen Prüfung in Länge von 30 Minuten erfolgen.
| Tag | Datum | Typ | Thema |
|---|---|---|---|
| Freitag | 23.10.20 | 1. Vorlesung | Introduction |
| Donnerstag | 29.10.20 | 1. Übung | Introduction |
| Freitag | 30.10.20 | 2. Vorlesung | Design-by-Contract mit JML |
| Donnerstag | 05.11.20 | 2. Übung | Design-by-Contract mit JML |
| Freitag | 06.11.20 | 3. Vorlesung | Advanced Specification with JML |
| Donnerstag | 12.11.20 | 3. Übung | Advanced Specification with JML |
| Freitag | 13.11.20 | 4. Vorlesung | Testing with JML |
| Donnerstag | 19.11.20 | 4. Übung | Testing with JML |
| Freitag | 20.11.20 | 5. Vorlesung | Software Model Checking with JPF |
| Donnerstag | 26.11.20 | 5. Übung | Software Model Checking with JPF |
| Freitag | 27.11.20 | 6. Vorlesung | First-Order Logic |
| Donnerstag | 03.12.20 | 6. Übung | First-Order Logic |
| Freitag | 04.12.20 | 7. Vorlesung | Sequent Calculus |
| Donnerstag | 10.12.20 | 7. Übung | Sequent Calculus |
| Freitag | 11.12.20 | 8. Vorlesung | Dynamic Logic |
| Donnerstag | 17.12.20 | 8. Übung | Dynamic Logic |
| Freitag | 15.01.21 | 9. Vorlesung | Deductive Verification with KeY |
| Donnerstag | 21.01.21 | 9. Übung | Deductive Verification with KeY |
| Freitag | 22.01.21 | 10. Vorlesung | Loops, Method Calls, and Inheritance |
| Donnerstag | 28.01.21 | 10. Übung | Loops, Method Calls, and Inheritance |
| Freitag | 29.01.21 | 11. Vorlesung | Correctness-by-Construction |
| Donnerstag | 04.02.21 | 11. Übung | Correctness-by-Construction |
| Freitag | 05.02.21 | 12. Vorlesung | Aktuelle Forschungsthemen im Bereich deduktive Verifikation |
| Donnerstag | 11.02.21 | 12. Übung | Experiment: Correctness-by-Construction |
| Freitag | 12.02.21 | 13. Vorlesung | Zusammenfassung |