Echtzeitsysteme werden in vielfältigen und ständig anspruchsvoller werdenden Anwendungsgebieten eingesetzt. Demzufolge nimmt die Komplexität von Echtzeitsystemen immer mehr zu. Gleichzeitig ist die korrekte Funktion eines Echtzeitsystems häufig sicherheitsrelevant (z.B. Airbagsteuerung, fly-by-wire Flugzeugsteuerung). Um die Korrektheit eines komplexen Systems garantieren zu können, reichen Tests, die nur einen Teil aller möglichen Eingaben abdecken, nicht aus, sondern es müssen formalere Methoden angewendet werden.
In dieser Vorlesung beschäftigen wir uns mit Techniken, mit denen Echtzeitsysteme formal modelliert und beweisbare Aussagen über deren Funktion getroffen werden können. Insbesondere untersuchen wir Zeitautomaten zur Modellierung von Echtzeitsystemen und eine Logik zur Formulierung von Eigenschaften von Echtzeitsystemen. Das Ziel der Vorlesung ist sowohl die Vermittlung theoretischer Grundlagen als auch deren praktische Anwendung am Beispiel des UPPAAL Systems.
Einige Fehler von Echtzeitsystemen
- Eisenbahn-Stellwerk Altona
-
1995 sollte das alte Stellwerk Altona mit 50 Angestellten
durch ein INTEL-486 Echtzeitsystem ersetzt werden.
Der Vorteil: Nur noch 10 Personen sind zum Betrieb nötig.
Nach Inbetriebnahme am 13.3.1995 kam es zum Absturz des Rechners.
Die Schließung des Stellwerks erzeugte ein Verkehrschaos
mit Auswirkungen im gesamten Bundesbahnverkehr.
Ursache: Bei starkem Zugverkehr versuchte das System einen Kellerspeicher (Stack) mit 4 kBytes im RAM-Speicher anzulegen. Benötigt und vorhanden waren eigentlich nur 3.5 kByte aber nicht 4 kByte. 500 Byte mehr wurden aus 'Sicherheitsgründen' reserviert!
Auswirkungen: Es war keine manuelle Ersatzsteuerung möglich! Die Reparatur durch den Hersteller Siemens erfolgte nach einigen Tagen durch das Hinzufügen von 0.5 Mega-Byte. Auch danach kam es noch Behinderungen bis die Angestellten das System beherrschten.
- Raumsonde Sojourner
-
Der Mars-Auto Pathfinder arbeitete erfogreich 1997
bis auf einen 'kleinen' Fehler:
Aus unerfindlichen Gründen bootete der Bordcomputer
und führte manchmal einen System-Neustart durch.
Der Verlust der gesammelten und noch nicht gespeicherten Daten
war die Folge. Die Ursache war die Organisation der Datenkommunikation
bei mehreren Anforderungen verschiedener Priorität:
'Prioritätsumkehr'.
Beschreibung: Der Informations-Bus ist als Shared-Memory-Bereich zur Datenübertragung zwischen verschiedenen Komponenten ausgelegt.
- Sei H ein Bus-Management-Task zum Datentransport mit der höchste Priorität und häufigem Auftreten.
- Sei N der Eintrag von meteorologischen Daten mit niederer Priorität und seltenem und kurzem Auftreten.
- Aber die Ausführung von N blockiert H (N wird nicht unterbrochen.)
- Sei M ein Kommunikations-Task mit mittlerer Priorität und langer Dauer.
- M bekommt Vorzug vor N, da M eine höhere Priorität hat.
- N wird ausgeführt;
- H will arbeiten, wartet aber auf das Ende von N;
- M tritt auf, unterbricht N, aber H ist weiter blockiert.
- Ein 'watchdog' bemerkt nach einiger Zeit, dass H nicht ausgeführt wird und befiehlt den Neustart des Systems.
- Das Denver-Koffer-Debakel
-
Bei der Neueröffnung des Flughafens in Denver sollte
ein voll automatisches Gepäcksystem verwendet werden.
Dieses System bestand aus etwa 300 Computern, Laserscannern,
Photozellen und einem Ethernet-Netzwerk.
Die Eröffnung des Flughafens verspätete sich wegen
Fehler im Gepäcksystem um 16 Monate.
Es kam zu zerquetschten und verlorenen Koffern, und es war
wieder die Gepäcksortierung per Hand nötig.
Verlust: ca. 3.2 Milliarden Dollar.
Teilursache: Zu viele Nachrichten wurden über das Ethernet-Netzwerk gesendet. Die Sortieranweisungen kamen nicht rechtzeitig wegen der Überlastung des Netzwerks an.
dn