Teilprojekt 6: Automotive

Teilprojekt 6 von Verisoft beschäftigt sich mit der Verifikation eines Automobilelektroniksystems. Das System besteht aus typischen Komponenten, die in Fahrzeugen eingesetzt werden: einem zeitgesteuertem Bussystem (ähnlich FlexRay) und einem zeitgesteuerten Betriebssystem (ähnlich OSEKTime). Auf diesen Systemkomponenten läuft als Anwendung ein automatisches Notrufsystem.

Verifikation von FlexRay

FlexRay ist ein high-end Echtzeit-Bus für Anwendungen aus dem Automobilbereich. FlexRay wird von einem Industriekonsortium führender Automobilhersteller und -zulieferer entwickelt und vorangetrieben. Der FlexRay-Standard spezifiziert ein Kommunikationsprotokoll. Insbesondere bietet dieses Kommunikationsprotokoll die folgenden beiden Eigenschaften:
  • Nachrichtentransfer mit periodischer, deterministischer Nachrichtenzustellung und
  • Synchronisation der Uhren aller an den Bus angeschlossenen Prozessoren (Knoten)

Im FlexRay Arbeitspaket geht es um die Implementierung und Verifikation von Schnittstellen zum FlexRay-Bus. Es soll gezeigt werden, dass diese Interfaces, angeschlossen an einen Kommunikationsbus, das FlexRay-Kommunikationsprotokoll einhalten und somit die erwähnten Eigenschaften besitzen.

Die Gatter-Implementierung dieser Interfaces ist abgeschlossen, mathematische Beweise für die Korrektheit liegen bereits vor. Es gilt nun letztere in Isabelle zu formalisieren.

Verifikation des OSEKtime Betriebsystems inklusive FTCom

OSEKtime ist ein Standard für ein zeitgesteuertes Betriebssystem, das eine Laufzeitumgebung für stark interagierende Echtzeitanwendungen in der Automobilelektronik bereitstellt. Es besteht aus einem präemptiven Dispatcher und einer fehlertoleranten Kommunikationsschicht FTCom. Ein Hauptentwurfsziel von OSEKtime ist die Vorhersagbarkeit der Ausführung. Daher wird das Scheduling zur Compilezeit statisch festgelegt.

FTCom ist eine fehlertolerante Kommunikationsschicht, die von OSEKtime bereitgestellt wird. Es ist für die Interaktion zwischen der Kommunikationshardware und der Anwendungssoftware zuständig. FTCom bietet eine Reihe von Diensten für die Anwendungsschicht und fungiert als Schnittstelle zum Bus Controller (in unserem Fall einem der oben erwähnten Interfaces). Die Dienste, die für die Anwendungen zur Verfügung gestellt werden, sind:

  • Verarbeitung globaler Nachrichten für die Kommunikation zwischen Anwendungen. Dies macht die Verteilung der Kommunikationspartner auf physikalische Prozessoren transparent, da FTCom sowohl lokal als auch global für die Übermittlung der Nachrichten sorgt.
  • Zeitdienst und externe Uhrensynchronisation für die Zeitkorrektur.

Im Zuge der Betriebsystem-Verifikation wurde OLOS, eine eingeschränkte Implementierung des OSEKtime Standards, entwickelt. Die Abkürzung OLOS steht für "OSEKtime Like Operating System". OLOS ist nicht für den fehlertoleranten Fall ausgelegt. Jedoch wurde besonderen Wert auf leichte Erweiterbarkeit gelegt, auch im Hinblick auf fehlertolerante Varianten.

Die Verifikation von OLOS ist angelaufen. Dies schließt auch die Verifikation der Kommunikationsschicht und der Gerätetreiber für die Interfaces mit ein.

Verifikation einer Anwendung

Die automatische Notrufanwendung, die vom Projektpartner BMW Group spezifiziert wurde, setzt nach dem Auftreten eines Unfalls einen Notruf bei einer Rettungsstelle ab. Hierfür liest die Notrufanwendung den Zustand des Crash-Sensor. Wenn der Crash-Sensor einen Unfall anzeigt, ermittelt die Anwendung über das Navigationssystem die Fahrzeugkoordinaten und sendet diese mit einem Mobiltelefon an eine Rettungsstelle. Die automatische Notrufanwendung interagiert also mit drei weiteren Anwendungen (Crash-Sensor, Navigationssystem und Mobiltelefon), die auf einzelnen ECUs laufen und über ein FlexRay-Netzwerk verbunden sind.

Die Anwendungen wurden in dem CASE-Tool AutoFocus als Automaten modelliert. Für diesen Zweck wurde ein spezielles Task-Modell entwickelt (AFTM, AutoFocus Task Model). AFTM erlaubt es, die Verifikation zu modularisieren. Für die Verifikation der Anwendung sind drei Schritte notwendig:

  • Verifikation des Task Modells für die konkrete Anwendung in AutoFocus (mittels Model Checking)
  • Beweis der korrekten Umsetzung des Task Modells in die Programmiersprache C0 (Translation Validation)
  • Beweis, dass die Ausführungssemantiken von AFTM und OSEKtime übereinstimmen.
AFTM erlaubt auch Schedule-Sysnthesis zur Abbildung von Tasks auf Prozesse, die unter OSEKtime laufen.

AutoFocus ist ein Werkzeug zur Modellierung verteilter Systeme. Ein System besteht aus einer Menge von Komponenten, die über Kommunikationskanäle verbunden sind und Nachrichten austauschen können. AutoFocus wurde an der Technischen Universität München, Fakultät für Informatik, Lehrstuhl IV: Software & Systems Engineering entwickelt.

 
Revision 14 Dec 2006