Safety Critical Systems 3, WS 2007/2008

Inhalt dieser Seite

• Termine
• Überblick
• Veranstaltungsinhalte
• Übungszettel
• Leistungsnachweise
• Literatur
• Software

Termine

Diese Veranstaltung wird (auf Wunsch) in Englisch gehalten. Trotzdem dürfen die Teilnehmer gerne Deutsch für ihre Aufgabenlösungen oder für Diskussionsbeiträge verwenden, falls sie möchten.

This course is held in English (on request). Nevertheless, participants are welcome to choose German for handing in assignments or for discussions, if they like.

Überblick

Sowohl für die Entwicklung als auch für VVT sicherheitskritischer Systeme ist es notwendig, ein präzises Modell zu haben, das das gewünschte Verhalten des Systems auf einer abstrakten Ebene beschreibt, d.h. ohne sich auf Implementationsdetails zu beziehen. In der Welt der sicherheitskritischen Steuerungssysteme umfassen die Steuerungsaufgaben oft sowohl diskrete als auch zeitkontinuierliche Observablen: Die ersteren haben einen endlichen Wertebereich und ändern sich zu diskreten Zeitpunkten (Schalter, Signale, Weichen, ...), während die letzteren (zumindest konzeptuell) stückweise kontinuierliche Funktionen über der Zeit sind (Temperatur, Druck, Schub, ...). Daher müssen Modellierungsformalismen in der Lage sein, sowohl diskrete als auch zeitkontinuierliche Aspekte auszudrücken. Hierfür werden wir Henzingers Definition Hybrider Automaten als allgemeinste Modellierungstechnik verwenden. Sie kann alle denkbaren Aspekte im Bereich sicherheitskritscher Echtzeitsysteme ausdrücken. Wir werden die theoretischen Begriffe der Safety- und Liveness-Bedingungen einführen und zum praktischen Begriff der sicherheitsrelevanten Zusicherung in Beziehung setzen.

Für ein konkretes Problem aus dem Gebiet der sicherheitskritischen Systeme kann es ratsam sein, weniger allgemeine Modelle als Henzingers Hybride Automaten zu verwenden:

Falls Safety-Aspekte durch Invarianten über diskrete Observablen und durch Bedingungen über sequentielle Variablentransformationen geeignet ausgedrückt werden können, dann ist die Z-Notation ein sinnvolles Mittel für die Spezifikation und formale Analyse dieser Aspekte. Falls Sicherheitsaspekte sich auf das kausale Verhalten eines Systems beziehen (Reihenfolge und Synchronisation von Ereignissen), dann ist CSP ein guter Kandidat für Spezifikation und VVT dieser Aspekte. Falls die Observablen diskret sind, aber Zeitbedingungen relevant sind, um Sicherheitsbedingungen auszudrücken, dann sind Timed-CSP und eine Anzahl von Timed-Automaten-Formalismen die geeignetsten Kandidaten für Modellierung und VVT.

Zumindest auf der intuitiven Ebene kann man die obigen Spezifikationsformalismen als Einschränkungen von Henzingers Hybriden Automaten ansehen. (Natürlich kann es auf einer formalen Ebene ziemlich schwierig sein, eine Spezifikation, die in einem dieser Formalismen geschrieben ist [wie etwa Z] in eine semantisch äquivalente Darstellung in einem anderen umzuwandeln [wie etwas Hybride Automaten].) Die praktischen Beispiele, die wir für die Modellierung von Sicherheitsaspekten von Steuerungssystemen verwenden werden, wählen wir aus der folgenden Liste:

• Die Fahrstuhlspezifikation: Sie ist ein Muss für jede Einführung in sicherheitsrelevante Systeme. Ihr bringt sie am besten in dieser Vorlesung hinter euch, sonst wird sie euch bis an das Ende eurer Tage verfolgen. Wir werden sie in Z modellieren und analysieren.
• Der Spiegelplattenalgorithmus: Ein einfaches Beispiel aus der Welt der fehlertoleranten Systeme. Es kann in CSP geeignet ausgedückt werden. Bei Bedarf können weitere Beispiele aus der Welt der Betriebssysteme gewählt werden.
• Sichere gepufferte Leser-Schreiber-Kommunikation in Echtzeit: Dies ist eine Menge von Standardmechanismen für den Datenaustausch zwischen Tasks in Echtzeitsystemen: Um sicherzustellen, dass die Kommunikation ohne Pufferüberlauf und ohne unzulässige Störung zwischen Leser und Schreiber stattfinden kann, ist es notwendig, den kommunizierenden Tasks Zeitrestriktionen aufzuerlegen. Hier benötigen wir einen Formalismus mit Zeit (Timed-Automata) für die Modellierung und Verifikation.
• Fishers Protokoll für gegenseitigen Ausschluss: Es realisiert den gegenseitigen Ausschluss zweier Tasks für deren kritische Abschnitte nur mit Hilfe einer gemeinsamen Variablen. Für diese wird nicht vorausgesetzt, dass sie atomar beschrieben und gelesen werden kann. Das Protokoll macht Annahmen über Zeitbedingungen, daher benötigen wir einen Formalismus mit Zeit.
• Das Bahnübergangsproblem: Es beinhaltet eine hybride Modellierung, denn man modelliert das Bremsen eines Zuges, das ihn daran hindert, in einen ungesicherten Übergang einzufahren, am besten mit differenzierbaren Funktionen.

Um die oben skizzierten Beispiele zu behandeln, können wir die folgenden Werkzeuge für die Modellierung und Analyse verwenden:

• Mike Spiveys Z-Type-Checker für die Z-Notation.
• Das FDR-Werkzeug zum Model-Checken von CSP ohne Zeit.
• Das UPPAAL-Werkzeug zum Model-Checken von Timed-Automaten.
• Das RT-Tester-Werkzeug zum automatisierten Testen und zur Simulation für CSP mit Zeit.
• Henzingers HYTECH-Werkzeug für die Analyse Hybrider Automaten.

Diese Werkzeuge sind für diese Vorlesung frei verfügbar. Die meisten davon können unter Linux benutzt werden.

Diese Vorlesung ist der dritte Teil der Vorlesungsserie "Safety-Critical Systems". Die Teile können in beliebiger Reihenfolge gehört werden.

• Safety-Critical Systems 1: Grundkonzepte - Probleme - Methoden - Techniken (WS 04/05, voraussichtlich SS 07)
• Safety-Critical Systems 2: Management-Aspekte - Standards - V-Modelle - TQM - Bewertung - Prozessverbesserung
• Safety-Critical Systems 3: Methods & Tools (dieses Semester)
• Safety-Critical Systems 4: Engineering of Embedded Software Systems (WiSe02/03)

Veranstaltungsinhalte

• Einführung in Z
  • Beispiel Fahrstuhlsteuerung
  • Konstanten-Deklaration - Typdeklaration - Spezifikation des Zustandsraums (Z-Schema) - Operations-Schema - Eingabeparameter - partielle Operationen - Invarianten - Inkludieren von Schemata
  • System-Anforderungen = Safety-Anforderungen + Benutzer-Anforderungen
  • Beweise von Eigenschaften - Aufschreiben von Beweisen
  • Beweistechniken: Kontraposition, Induktion
  • das Werkzeug fuzz
• Umsetzung von Z-Operations-Schemata in Implementierungen
  • Scheduling der Operationen
  • Behandlung von Z-Inputs in der Implementierung
  • Zeitbedingungen
  • Abbildung mathematischer Datentypen
  • Umsetzung impliziter Operationsspezifikationen
• Einführung in CSP
  • Beispiel Spiegelplattentreiber
  • Strukturierung in parallele, kommunizierende Prozesse
  • Paralleloperatoren
  • Watchdogs
  • das Werkzeug FDR2
• Einführung in Timed Automata
  • Sprachelemente zur Modellierung: Locations, Transitions, Guard Conditions, Synchronisation durch Kanüle, Update-Operationen, Clocks, Clock-Invariants, globale und lokale Variablen,
  • Sprachelemente für temporal-logische Zusicherungen: A[]phi, E[]phi, A<>phi, E<>phi, phi --> psi
  • Testautomaten (`Watchdogs') als Alternative zu komplexen A[]phi und E[]phi-Formeln
  • das Werkzeug UPPAAL
  • Fallstudien:
    • Fischers Protokoll
    • Train Gate
  • Modellbasierte Entwicklung mit Timed Automata: Systematische Transformation von Timed Automata in Code

Hintergrundmaterial

• Specification of an elevator in Z:
  • 1st version: pdf - fuzz/LaTeX source
  • final: pdf - fuzz/LaTeX source
• Z Reference Card
• Z Manual
• Mirrored disk driver (CSP specification)
• Fault-tolerant server system (Habilitationsschrift, Kapitel 3.3)
• Beispiel für Prüfautomaten mit UPPAAL
• Modellierung und Verifikationsbedingungen für das Non-Blocking Write Protocol mit UPPAAL
• Hybrid Automata: HyTech Model Checker, Railroad Crossing Example

Übungszettel

Leistungsnachweise

• Entweder durch erfolgreiches Bearbeiten von Übungsaufgaben inkl. bestandenem Fachgespräch,
• oder durch eine bestandene mündliche Prüfung (alias mündliche Modulprüfung).

Die genauen Bedingungen werden in der ersten Vorlesung verhandelt.

Literatur

Software

• fuzz 2000 - Mike Spivey's type checker for Z:
  • installation on your computer:
    • Download the gzipped tar file.
    • Follow the instructions in the INSTALL file.
• UPPAAL - editor, simulator and model checker for Timed Automata:
  • Installation instructions
  • Tutorial