Inhaltsüberblick für Safety-Critical Systems 3: Methods & Tools, WoSe 2003

Diese Veranstaltung wird (auf Wunsch) in Englisch gehalten.

Wir konzentrieren uns auf konkrete Probleme, die in bestimmten Arten von sicherheitskritischen Systemen entstehen, und auf Methoden und Werkzeuge, die geeignet sind, diese Probleme zu modellieren, zu verifizieren, zu validieren und zu testen (VVT).

Sowohl für die Entwicklung als auch für VVT sicherheitskritischer Systeme ist es notwendig, ein präzises Model 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 Muß 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, daß 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-Automaten) für die Modellierung und Verifikation.
• Fishers Protokoll für gegenseitigen Ausschluß: Es realisiert den gegenseitigen Ausschluß zweier Tasks für deren kritische Abschnitte nur mit Hilfe einer gemeinsamen Variablen. Für diese wird nicht vorausgesetzt, daß 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 (SoSe02)
• Safety-Critical Systems 2:
  Management-Aspekte - Standards - V-Modelle - TQM - Bewertung - Prozeßverbesserung (SoSe01)
• Safety-Critical Systems 3: Methods & Tools (dieses Semester)
• Safety-Critical Systems 4: Engineering of Embedded Software Systems (WiSe02/03)