MMISS - MultiMedia-Instruktionen in Sicheren Systemen

Ziel des Projektes ist die Erstellung eines multimedialen, internetgestützten, adaptiven Lehr- und Lernsystems für die Informatikausbildung. Es wird das gesamte Curriculum des Fachgebiets "Sichere Systeme" abdecken, ein Gebiet von hoher industrieller und gesellschaftlicher Relevanz. Es soll im normalen Lehrbetrieb der beteiligten Universitäten und im Sommerstudium für Frauen "Informatica Feminale" eingesetzt werden. Darüber hinaus wird es auch für andere deutsche und europäische Universitäten und für industrielle Weiterbildungsmassnahmen zur Verfügung stehen.

Das System bietet eine konsistente, hypermediale Aufbereitung von klassischen Vorlesungsmaterialien (Folien, Büchern, Skripten, Übungsaufgaben etc.) und eine Integration von Werkzeugen zur formalen Entwicklung korrekter Software und ist damit sowohl zur Unterstützung der Präsenzlehre, zum Fernstudium als auch zum interaktiven, betreuten und kooperativen Selbststudium geeignet.

Besonderer Wert wird auf Kohärenz und Konsistenz der Inhalte durch umfassende semantische Vernetzung gelegt. Dazu wird ein aus der formalen Softwareentwicklung entlehntes semantisch geprägtes Vorgehensmodell zur Erweiterung der Wissensbasis mit Versions- und Konfigurationsmanagement eingesetzt; damit soll insbesondere die nachhaltige Pflege der Lehrinhalte gewährleistet werden.

Weitere Informationen zur BMBF-Förderung "Neue Medien in der Bildung" können Sie unter http://www.medien-bildung.de nachlesen.

Projektpartner

Das MMISS-Projekt wird durch das Minitsterium für Bildung und Forschung (BMBF) finanziert. An der Durchführung sind die folgenden Universitäten beteiligt:

Beteiligte Personen der LMU München

Inhalte der LMU München

Die LMU München wird folgende Lehrinhalte zum MMISS-Projekt beisteuern (in der Klammer nach dem Titel werden die für diese Vorlesung federführenden Personen genannt):

Formale objektorientierte Software-Entwicklung (Wirsing, Hennicker)

Software-Engineering kann sich im Bereich der Sicherheit und Verlässlichkeit noch keineswegs mit anderen Ingenieurdisziplinen messen. In der Vorlesung wird darauf eingegangen, wie diese Kluft überbrückt werden kann, indem pragmatische Methoden der objektorientierten Software-Entwicklung durch fundierte, formale Techniken ergänzt werden. Als Modellierungssprache wird hierbei die Unified Modeling Language UML verwendet. Für die formale Beschreibung von Eigenschaften objektorientierter Systeme wird die Object Constraint Language OCL eingesetzt. In diesem Rahmen werden Spezifikationsmethoden und Validierungstechniken für Systemmodelle besprochen und Methoden zum Nachweis der Korrektheit von Verfeinerungen und Implementierungen vorgestellt.

Grundlagen der Systementwicklung (Wirsing, Merz)

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, CASL)
Spezifikation dynamischer Systeme (Transitionssysteme, modell-basierte Spezifikationen, Invarianten, Vor- und Nachbedingungen, Z)
Verifikation und Verfeinerung nebenläufiger Systeme (Eigenschaften von Abläufen, Temporale Logik, Model Checking, TLA)

Temporale Logik und Zustandssysteme (Kröger, Merz)

Zustandssysteme (in mehr technischer Sprechweise: Zustandsübergangssysteme) bilden einen sehr allgemeinen Sammelbegriff für alle Arten von Systemen, die ablaufen können, wobei ein Ablauf eine Folge von Zuständen ist. Beispiele (aus der Informatik) sind Programme bzw. allgemeinere Software-Systeme, Schaltkreise, Datenübertragungsprotokolle, Automaten, Petri-Netze usw. Temporale Logik ist eine Erweiterung der klassischen mathematischen Logik, bei der Aussagen in verschiedenen Zuständen (Zeitpunkten) verschiedene Wahrheitswerte haben können. Sie eignet sich somit als logische Grundlage zur formalen Behandlung von Zustandssystemen. Die Vorlesung gibt eine ausführliche Einführung in verschiedene Varianten dieser Logik (hauptsächlich lineare und verzweigte Temporallogik sowie TLA) und entwickelt systematisch ihre Anwendungsmöglichkeiten im Bereich der Spezifikation und Verifikation (einschließlich model checking) von Systemen. Als spezielle Anwendung wird die Verifikation paralleler Programme behandelt.

Model Checking (Merz)

Unter Model Checking versteht man Verfahren zur automatischen Analyse reaktiver Systeme wie etwa eingebetteter Steuerungen (z.B. Airbagauslösung im Auto) oder Kommunikations- und kryptographische Protokolle (z.B. das Needham-Schroeder public-key Protokoll). Auf Grund der Vielzahl von möglichen Abläufen, die zu nicht oder nur schwer reproduzierbaren Fehlersituationen führen ("race conditions") ist die Entwicklung reaktiver Systeme traditionell sehr fehleranfällig. Andererseits kommen solche Systeme häufig dort zur Anwendung, wo Fehler teuer sind oder sogar eine Gefährdung von Leib und Leben bedeuten können. Es wurden daher verschiedene Techniken entwickelt, mit denen Modelle reaktiver Systeme rechnergestützt auf kritische Eigenschaften überprüft werden können. Dabei werden alle möglichen Abläufe des Modells betrachtet, so dass eine weit bessere Fehlerabdeckung erreicht werden kann als durch bloße Testläufe. Model Checking wird mittlerweile in der Industrie (etwa bei Intel, IBM, Siemens, AT&T und Motorola) routinemäßig eingesetzt und auch weiterentwickelt. Auch im Fahrzeug- und Flugzeugbau, im Bereich Consumer Electronics sowie allgemein bei Prozess-Steuerungen werden derzeit Modelchecking-Verfahren erprobt und evaluiert. Bewerber mit entsprechendem Hintergrund haben exzellente Chancen in den betreffenden Entwicklungsabteilungen.