Safety Critical Systems 3, SoSe 2005

! Diese Vorlesung fällt in diesem Semester aus, wird aber im nächsten Semester stattfinden !

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 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)

Veranstaltungsinhalte

Ü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

• installation on your computer:
  • Download the gzipped tar file.
  • In general, follow the instructions in the INSTALL file.
  • You will probably have to change two paths in the Makefile. On current Linux versions, you need:
    TEXDIR=/usr/share/texmf/tex/local
    MFDIR=/usr/share/texmf/fonts/source/local
    The ".../local" final parts do not exist yet, so you must create these two directories with "mkdir" before issuing "make install"!
    
  • If you change LIBDIR to something else than /usr/local/lib, you must do the following to the Makefile, too:
    Add the line:

    CFLAGS=-DDEFAULT=\"$(LIBDIR)/fuzzlib\" -DENVNAME=\"FUZZLIB\"

    Change the line

        $(MAKE) -C $@ all

    to

        $(MAKE) 'CFLAGS=$(CFLAGS)' -C $@ all

  • The bison grammar of Z contains three small problems. Older versions of bison don't care, such as bison 1.28 from SuSE Linux 7.3. But the current bison 1.75 refuses to compile the file src/zparse.y. Therefore please fix: in lines 117 and 239, append a semicolon to the line; and in line 267, replace "@2.line" by "@1.line".
• using the Linux computers x01 - x31 in Ebene 0 of the MZH building:
  • set up LaTeX for typesetting:
    

    source texsetup.sh

    (This switches from the local to the global LaTeX version.)
  • set up the path for running the type checker:
    

    export PATH="${PATH}:/home/brederek/pub/fuzz2000/linux-i386/bin"