SucheFormale Methoden im Software Engineering SS 2012
| Titel: | Formale Methoden im Software Engineering |
| Dozent(in): | Dominik Haneberg, Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst |
| Termin: | Vorlesung Montag 10:00 - 11:30 |
| Gebäude/Raum: | Vorlesung im 1057 N. Übung im 3017 N |
| Anmeldung: | Anmeldung erfolgt in der ersten Vorlesung am 16.4.2012. Eine nachträgliche Anmeldung ist nicht mehr möglich. Die Übungen finden in Zweier-Gruppen statt. |
Downloads:
Vorkenntnis für die Lehrveranstaltung:
Interesse an Logik und formalen Methoden, Bachelorveranstaltung Logik für Informatiker ist hilfreich
Literatur zur Lehrveranstaltung:
Es besteht eigentlich keine Notwendigkeit, zusätzliche Literatur heranzuziehen. Wer sich dennoch etwas schlauer machen will, kann folgende Bücher lesen:- V. Sperschneider and G. Antoniou, Logic: A Foundation for Computer Science, Addison Wesley, 1991
- J. Loeckx and H.D. Ehrich and M. Wolf, Specification of Abstract Data Types, Wiley-Teubner, 1996
Der Lehrstuhl Softwaretechnik und Programmiersprachen bietet im SS 2012 die Veranstaltung "Formale Methoden im Software Engineering" (integrierte V + Ü) an.
Die Verwendung formaler Methoden bei der Entwicklung korrekter Software steht an der Schwelle der kommerziellen Nutzung. Das KIV-System ist ein Werkzeug, das die formale Spezifikation, Verifikation und Synthese von Programmen ermöglicht. Es wird seit mehreren Jahren entwickelt und inzwischen in industriellen Studien erprobt. Übergeordnetes Ziel ist die Produktion beweisbar korrekter Software.
Die Lehrveranstaltung vermittelt den ''state of the Art'' des Einsatzes formaler Methoden bei der Softwareentwicklung. Es werden Spezifikationstechniken zur Beschreibung und Methoden zum Nachweis der Korrektheit von Softwaresystemen behandelt. Die Lehrveranstaltung beginnt mit der (algebraischen) Spezifikation von Datentypen und stellt dann Kalküle und Vorgehensweisen für die Verifikation sequentieller und paralleler Programme vor. Weiterhin wird Refinement als systematisches Entwicklungsvorgehen von einer abstrakten Spezifikation zu einer korrekten Implementierung vorgestellt.
Die Rechner im Raum 3017N stehen auch außerhalb der Praktikumszeiten zur Verfügung. Notfalls bei uns nach einem Schlüssel fragen, falls der Raum abgesperrt ist.
Wichtig: Der/die Letzte der abends geht, muss dafür sorgen, dass der Raum abgesperrt wird. Typischerweise dazu bei einem Mitarbeiter des Lehrstuhls vorbeigehen.
Termine für das Praktikum
Das Praktikum findet jeweils am Freitag statt.| 8:15-9:45 | 10:00-11:30 | 14:00-15:30 | 15:45-17:15 | |
|---|---|---|---|---|
| Gruppe 1 | x | x | ||
| Gruppe 2 | x | x | ||
| Gruppe 3 | x | x | ||
| Gruppe 11 | x | x | ||
| Gruppe 12 | x | x | ||
| Gruppe 13 | x | x | ||
| Gruppe 14 | x | x |
weitere Informationen zu der Lehrveranstaltung:
| empfohlenes Studiensemester der Lehrveranstaltung: | Master |
| Fachrichtung Lehrveranstaltung: | Informatik (Dipl., Bachelor, Master) |
| Dauer der Lehrveranstaltung: | 6 SWS |
| Typ der Lehrveranstaltung: | WV - Wahlvorlesung |
| Leistungspunkte: | 8 LP für Vorlesung und Praktikum |
| Bereich: | (MA neue PO) Softwaretechnik; (alte POs) Softwaretechnik, Theoretische Informatik |
| Prüfung: | Sonstige |
| Lehrveranstaltungspflicht: | Wahlpflicht |
| Semester: | SS 2012 |