Grundlagen der Systementwicklung
Prüfungstermine
Mittermüller | Simon | 10:00 |
Krpan | Leonard | 10:00 |
Frankenberger | Florian | 10:00 |
Sommer | Oliver | 11:00 |
Moutschka | Eva | 11:00 |
Mauder | Markus | 11:00 |
Kraft | Harald | 12:00 |
Promesberger | Robin | 12:00 |
Grupp | Nico | 13:30 |
Marcus | Philipp | 13:30 |
Bui | Hai-Lam | 13:30 |
König | Benjamin | 14:30 |
Göppner | Benedikt | 14:30 |
Zauner | Harald | 14:30 |
Prüfungsformalitäten
- Datum: Mittwoch, 13. Februar, ab 14:00 Uhr.
- Anmeldung: Per E-Mail (Axel.Rauschmayer (a) ifi.lmu.de).
- Frist: Bitte bis Montag, 11. Februar anmelden.
- Pro Student benötigen wir folgende Angaben:
- Vor- und Nachname
- Matrikelnummer
- Geburtsdatum
- Hauptstudium
- Als Antwort bekommen Sie einen Termin zugewiesen.
- Die Prüfung ist mündlich, es werden 3 Studierende in einer Stunde (notfalls 2 Studierende in 40min) geprüft.
- Gruppenbildung: Sie können auch Dreiergruppen bilden, dann bitte alle Studierenden-Datensätze in einer E-Mail schicken.
Aktuelles
Zeitplan bis Ende des Semesters:6.2. Mi | Vorlesung |
7.2. Do | Übung |
8.2. Fr | Letzte Vorlesung |
13.2. Mi |
Mündliche Prüfungen (ab 14:00 Uhr) |
Inhalt
Ein bedeutsames und derzeit noch unbefriedigend beherrschtes Problem im Entwicklungsprozess technischer Systeme ist die Zuverlässigkeit der produzierten Software. Diese ist gegeben, wenn ein Softwaresystem im Sinne der Aufgabenstellung funktioniert und auch auf Fehler angemessen reagiert. Besonders in sicherheitskritischen Anwendungsgebieten, wie etwa bei medizinischen Anwendungen, bei Zahlungssystemen, elektronischer Kommunikation, Zugangskontrollsystemen, aber auch Gasbrennersteuerungen im Haushalt, ist es entscheidend, dass die verwendeten Programmsysteme zuverlässig und sicher arbeiten. Die Vorlesung gibt eine Einführung in Methoden und Techniken zum Entwurf sicherer Systeme. Besonderes Gewicht wird dabei auf Techniken der Spezifikation und der Verfeinerung von Spezifikationen gelegt, die die Grundlage für moderne Validierungs- und Verifikationswerkzeuge bilden. Insbesondere werden folgende Themen behandelt:
- Daten-orientierte Spezifikationsentwicklung (Abstrakte Datentypen, Wechsel der Datenstruktur)
- Spezifikation dynamischer Systeme (Transitionssysteme, modell-basierte Spezifikationen, Invarianten, Vor- und Nachbedingungen)
- Verifikation und Verfeinerung nebenläufiger Systeme (Eigenschaften von Abläufen, Temporale Logik, Model Checking, TLA)
Hörerkreis
Studierende im Haupt- und Nebenfach Informatik
Benötigte Vorkenntnisse
Grundkenntnisse in Informatik und Logik
Scheinerwerb
Wird noch bekannt gegeben
Literaturhinweise
- Algebraische Spezifikationen
-
J. Loeckx, H. Ehrich, M. Wolf. Specification of Abstract Data Types. Wiley & Teubner, 1996.
-
M. Wirsing. Algebraic specification. In: J. van Leeuwen (ed.). Handbook of Theoretical Computer Science. Elsevier, Amsterdam, 1990.
-
C. Morgan. Programming from Specifications. Prentice Hall, 3. Auflage, 1998. Es gibt eine "web edition".
- CCS
- Robin Milner. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, 1. Auflage, 1999.
- TLA
- L. Lamport. TLA-Homepage.
-
Z. Manna, A. Pnueli. The temporal logic of reactive and concurrent systems - specification. Springer-Verlag, New York, 1992 (vergriffen, in der Bibliothek vorhanden).
-
L. Lamport. TLA - The Temporal Logic of Actions.