Materialien
Vorlesungsmaterial
Seminar: Model Checking - Probabilistische und Echtzeitaspekte - Sommersemester 2010
Übersicht
| Beschreibung |
Das Seminar behandelt zwei Themengruppen, die aktuelle Forschungsthemen in der Verifikation von eingebetteten Systemen darstellen: Probabilistische und Echtzeitsysteme. (a) Echtzeitsysteme: Bei reaktiven Systemen wie z.B. Kommunikationsprotokollen oder Bankautomaten müssen Ergebnisse unter gewissen Zeitbedingungen berechnet werden. Eine Methode, um das Verhalten von sogenannten zeitkritischen Systemen zu modellieren, sind Zeitautomaten (engl.: Timed Automata), eine Erweiterung von klassischen Zustandsautomaten um sogenannte Clockvariablen und Zeitbedingungen. In diesem Semniar sollen verschiedene Aspekte zur Modellierung und Verifikation von Timed Automata ausgearbeitet werden: * Grundlagen Timed Automata * TCTL und Modelchecking * Difference Bound Matrices und UPPAAL * Clock Difference Diagrams * Bounded Model Checking (b) Probabilististische Systeme In vielen F"allen kann nicht garantiert werden, dass eine Eigenschaft unter allen Umständen gilt, beispielsweise weil die endliche Lebensdauer von Komponenten berücksichtigt werden muss oder die Kommunikation zwischen Systemen über unzuverlässige Funkverbindungen erfolgt, was dazu führen kann, dass Nachrichten verloren gehen oder verstümmelt werden. Puffer, die Daten vor der Verarbeitung zwischenspeichern, können überlaufen, wenn die Daten schneller eintreffen, als sie verarbeitet werden können. Beschränkt man sich bei der Verifikation auf qualitative Eigenschaften (das heißt solche, die entweder gelten oder nicht), so müsste man in allen Fällen das System als inkorrekt ansehen: selbst wenn während eines Fluges mehrere Systeme gleichzeitig ausfallen müssen, damit ein sicherheitskritischer Zustand erreicht wird, kann dieser Fall nicht mit absoluter Sicherheit ausgeschlossen werden. Dass Nachrichten, wenn sie über unzuverlässige Medien versendet werden, verloren gehen oder nur verstümmelt ankommen, ist meist unvermeidlich, denn zuverlässige Kommunikationsmedien sind oft nicht verfügbar oder zu teuer zu realisieren. Kennt man die maximale Rate, mit der Daten eintreffen nicht genau, so müsste die Kapazität des Puffers unbeschränkt groß sein, damit garantiert werden kann, dass der Puffer nie überläuft. Deshalb ist man an quantitativen Aussagen interessiert: Ist die Wahrscheinlichkeit, bei einem 10-stündigen Flug in einen sicherheitskritischen Zustand zu gelangen, kleiner als 10-6? Wie groß ist die Wahrscheinlichkeit, dass der Informationsaustausch per Funkverbindung mit höchstens 5 Nachrichten gelingt? Wie groß muss die Puffergröße gewählt werden, damit die Wahrscheinlichkeit, mehr als 0.1 % der Daten verwerfen zu müssen, kleiner als 1 % ist? Themen aus diesem Bereich der Verifkation umfassen: * Einführung in Markow-Ketten und wichtige Eigenschaften * Model Checking für Markow-Ketten mit diskreter Zeit * Model Checking für Markow-Ketten mit kontinuierlicher Zeit * Gegenbeispiele für Markow-Ketten * Model Checking für parametrische Markow-Ketten |
| Kommentar |
|