Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > SoSe 2003 > Deutsch
English
 

Safety-Critical Systems 3: Methods & Tools, SoSe 2003
 

Veranstalter / read by: Jan Peleska, Jan Bredereke

Termine:
V: Di. 10-12 Uhr, GW2 B2180
Ü: Do. 10-12 Uhr, MZH 8090 (geändert!)

dates:
lecture: Tue 10-12 am, GW2 B2180
seminar: Thu 10 am - 12 noon, MZH 8090 (changed!)

ECTS: 6

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. Es gibt auch einen deutschen Inhaltsüberblick.

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.

Context of the Safety-Critical Systems Lectures Series

This is a series of lectures and seminars of our initiative Graduate Studies in Safety-Critical Systems. It is intended for an international audience of engineers working in the field, graduate students working on their Diploma, Masters, PhD or Habilitation degrees in computer science or electrical engineering. Due to the international character of the initiative, lectures will be held in English. At present, the lecture series is divided into four parts, each part planned as a two plus two hours/week lecture for one term:

  • Safety-Critical Systems 1:
    Basic concepts - problems - methods - techniques (SoSe02 term)
  • Safety-Critical Systems 2:
    Management aspects - standards - V-Models - TQM - assessment - process improvement (SoSe01 term)
  • Safety-Critical Systems 3: Methods & Tools (this term)
  • Safety-Critical Systems 4: Engineering of Embedded Software Systems (WiSe02/03 term)

These parts can be attended in any order.

The first three parts are read by Jan Peleska, the fourth one is read by Jan Bredereke.

Objectives and Summary of the Safety-Critical Systems 3 Lecture

We focus on concrete problems arising in specific types of safety-critical systems, and methods and tools which are suitable for modelling, verification, validation and test (VVT) of these problems.

Both for the development and for VVT of safety-critical systems, it is mandatory to have a precise model describing the intended behaviour of the system on an abstract level, that is, without referring implementation details. In the world of safety-critical control systems, the control tasks often involve both discrete and time-continuous observables: The former have a finite domain and change at discrete points in time (switches, traffic lights, points, ...) while the latter are (at least conceptually) piecewise continuous functions over time (temperature, pressure, thrust, ...). As a consequence, the modelling formalisms must be capable of incorporating both the discrete and time-continuous aspects. To this end, we will use Henzinger's definition of Hybrid Automata as the most general modelling technique which can be used to capture all possible aspects in the context of safety-critical real-time systems we can think of. The theoretical notions of safety conditions and liveness conditions will be introduced and related to the practical notion of safety-related assertions.

For a concrete problem from the field of safety-critical systems it may be advisable to use less general models than Henzinger's Hybrid Automata:

  • If safety aspects may be properly expressed by invariants on discrete observables and by conditions on sequential variable transformations, the Z notation provides a practical means for specification and formal analysis of these aspects.
  • If safety aspects refer to the causal behaviour of a system (sequencing and synchronisation of events), CSP is an appropriate candidate for specification and VVT of these aspects.
  • If observables are discrete, but timing constraints are relevant to express safety conditions, Timed CSP and a number of Timed Automata formalisms are the most suitable candidates for modelling and VVT.

At least on an intuitive level the specification formalisms listed above can be viewed as restrictions of the Henzinger's Hybrid Automata. (Of course, on a formal level, it may be quite hard to map a specification written in one formalism [such as Z] into a semantically equivalent representation in another one [such as Hybrid Automata].) The practical examples to be used for modelling safety-related aspects of control systems are chosen from the following list:

  • The elevator specification: this is a must when introducing safety-related systems. You better get over it in this lecture, otherwise it will haunt you until the end of your days. This will be modelled and analysed in Z.
  • The Mirrored Disk algorithm: A simple example from the world of fault-tolerant systems, may be adequately modelled using CSP. Further examples can be selected on demand from the world of operating systems.
  • Safe buffered Reader-Writer Communication in real-time: This is a set of standard mechanisms used for data exchange between tasks in real-time systems: To ensure that communication will take place without buffer overflow and without illegal interference between readers and writers, it is necessary to impose some timing restrictions upon the communicating tasks. Here we need a formalism with time (timed automata) for modelling and verification.
  • Fisher's mutual exclusion protocol: It implements the mutual exclusion of the critical sections of two tasks, using a shared variable only. It does not require atomic read and write access. The protocol makes assumptions about timing, therefore we need a formalism with time.
  • Railway crossing problem: This involves hybrid modelling, since braking a train to prevent it from running into an unsafe crossing is best modelled by differentiable functions.

To tackle the examples sketched above, we may use the following tools for modelling and analysis:

  • Mike Spivey's Z type checker for the Z notation
  • The FDR tool for model checking untimed CSP.
  • The UPPAAL tool for model checking timed automata.
  • The RT-Tester tool for automated test and simulation with Timed CSP.
  • Henzinger's HYTECH tool for the analysis of Hybrid Automata.

The tools are freely available for this lecture. Most of them can be used with Linux.

The course is intended for advanced students of computer science or electrical engineering who already know to program and maybe have some first experience in a software project.

Detailed Contents of the Lecture
  • Einführung in Z
    • Beispiel Fahrstuhlsteuerung
    • Beispiel Geburtstagskalender
    • 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-Struktur für sicherheitsrelevante Systeme: prioritäten-gesteuertes, präemptives Scheduling - zyklisches, sequentielles Scheduling (nicht präemptiv)
    • siehe die Mitschrift der Vorlesung am 20.5.2003 (ps/gzip - pdf).
    • Behandlung von Z-Inputs in der Implementierung
      • Input-Techniken: synchron, interrupt-gesteuert - Polling (DMA, Kartenregister lesen, dual-ported RAM)
      • Ankopplung von Events an das zustandsbasierte Modell von Z: Ringpuffer
  • Fehlertoleranz
    • im Gegensatz zur Fehlervermeidung
    • Degradation - Recovery - Redundanz - Fail-Stop - Fault Containment
    • Fehlertoleranz für Sicherheit / für Verfügbarkeit
    • siehe auch die Folien zur Vorlesung SCS1 im SoSe02
  • Einführung in CSP
    • Beispiel Spiegelplattentreiber
    • Strukturierung in parallele, kommunizierende Prozesse
    • Paralleloperatoren
    • Watchdogs
    • das Werkzeug FDR2
    • Beispiel Kaffee- und Teemaschinen
    • Verfeinerung: Trace-Verfeinerung - Failure-Verfeinerung (nicht prüfungsrelevant)
  • Verifikationstechniken
    • Watchdogs
    • [Prozeß-Vergleich (Refinement)]
    • Erreichbarkeitsanalyse
  • Einführung in Hybride Automaten
    • Beispiel Fishers Mutex-Protokoll
    • Beispiel Bahnübergang
    • Beispiel Non-Blocking-Write-Protokoll
    • Beispiel Water-Level-Controller
    • das Werkzeug HyTech
    • Zustandsraum - Regionen - Konvexität
    • automatisches Berechnen von Timing-Parametern
    • physikalisches Modell - Controller-Modell
    • Zustandsexplosion - Heuristiken zur Vermeidung
    • Validation der Spezifikation: alle Locations erreichbar?
  • Von Z & CSP (automatisch?) zum ausführbaren Programm
    • automatische Compilierung von SQL perfekt gelöst
    • für Z nicht allgemein, aber in vielen speziellen Fällen lösbar
    • für CSP weitgehend durch Umsetzung nach Occam gelöst
    • Umsetzung von CSP-Datentypen nach C/C++/Java
    • Umsetzung von Z-Datentypen nach C/C++/Java
    • Umsetzung operationeller Z-Schemata nach C/C++/Java - Determinismus bei sicherheitsrelevanten Systemen
    • Traceability der Umsetzung
    • Umsetzung von CSP-Prozessen nach C/C++/Java - zum Beispiel mit Threads - Kommunikation über Sockets

Slides

None - we used the good old blackboard...

Specifications Used in the Course

Assignments

Mark ("Schein")

Criteria negotiated by lecturer and participants on Apr. 29, 2003:

  • assignments can be solved in groups of two or three
  • average of marks must be >= 60%
  • oral exam ("Fachgespräch") at end of term
    • in the groups of two/three
    • individual marks

Text Worth Reading

More references will be introduced during the course.

Software
  • fuzz 2000 - Mike Spivey's type checker for Z:
    • 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"
  • FDR2 - Formal System Ltd.'s model checker for CSP:
  • HyTech vers. 1.04f - Thomas A. Henzinger's model checker for Hybrid Automata: gzipped tar file
    The executable files in the directory HyTech-1_04f/bin are ready to run under Linux. You will have to recompile the source for other platforms. The user guide and examples are contained in the tar archive, too. Further information on Hybrid Automata and Henzinger's HyTech tool can be obtained from http://www-cad.eecs.berkeley.edu/~tah/HyTech/

Related Activities of Other Groups and Organisations

 		 
   
Autor: jp 		 
  AG Betriebssysteme, Verteilte Systeme 
Zuletzt geändert am: 2. November 2022   Impressum