Navigationsmenü

Entwicklung korrekter Systeme

[English]

Sie sind hier: Uni . Fk. II . Informatik . theoretica . CSD . Lehre . FP. Realzeitsysteme . Ergebnis

Entwicklung korrekter Systeme

Fortgeschrittenen-Praktikum ``Realzeitsysteme''

Ergebnisbericht

Auf dieser Seite

Einleitung
Verlauf des Praktikums
Abschlussprojekt ``Zugsteuerung''
Teilnehmer

zurück zur Hauptseite.

1 Einleitung

Das Fortgeschrittenen-Praktikum "Realzeitsysteme" (Ankündigung) wurde im Wintersemester 2000/2001 an der Carl-von-Ossietzky Universität Oldenburg unter Leitung von Dr. Henning Dierks durchgeführt. Es nahmen fünf StudentInnen aus dem Hauptstudium daran teil (siehe Teilnehmer), welche sich zunächst in zwei Gruppen aufteilten.

Bei Realzeitsystemen spielt die Zeit, in welcher bestimmte Aktionen durchgeführt werden müssen, eine große Rolle. Zum Beispiel müssen Maschinen innerhalb einer bestimmten Zeitschranke auf externe Ereignisse (etwa Sensordaten) reagieren und eine entsprechende Aktion auslösen. Im Praktikum wurde gezeigt, wie man solche Systeme modellieren und verifizieren kann. Zusätzlich wurden Realzeitprogramme für Lego Mindstorms Roboter simuliert und implementiert. Für die Lego Mindstorms (auch "RCX" genannt) existiert ein freies Betriebssystem namens LegOS, welches C-Programme ausführen kann. Diese Programme wurden entweder "per Hand" geschrieben oder von Moby/PLC (einem Tool zur Entwicklung von Kontrollprogrammen für speicherprogrammierbare Steuerungen) generiert.

2 Verlauf des Praktikums

In den ersten drei Übungen wurde die zu benutzende Hardware-Plattform (RCXe mit LegOS) vorgestellt, dh. es wurden C-Programme entwickelt, kompiliert und auf den RCXen ausgeführt. Insbesondere wurde auch die Kommunikation zweier RCXe über die Infrarot-Schnittstelle benutzt.

Danach kamen wir zur formalen Verifikation von Realzeitautomaten mittels Uppaal. Dabei wurden Systeme als Realzeitautomaten in der entsprechenden Syntax spezifiziert und dann mit Hilfe von Uppaal auf gewisse wünschenswerte Eigenschaften getestet.

Dann kam das bereits erwähnte Moby/PLC zum Einsatz. Mit diesem Tool können PLC-Automaten graphisch modelliert und simuliert werden. Es kann sowohl LegOS- wie auch Uppaal-Code automatisch generieren, wodurch dann die Systeme mittels Uppaal verifiziert und auf den RCXen ausgeführt werden können.

Am Ende stand eine größere Abschlussaufgabe, welche von allen Teilnehmern gemeinsam gelöst wurde.

3 Abschlussprojekt ``Zugsteuerung''

Die Aufgabenstellung bestand darin ein Gleissystem aus Lego-Schienen zu konstruieren, auf welchem zwei Lego-Züge (zwei RCXe) fahren sollen. Ein kritischer Bereich, in welchen beide Züge einfahren können, sollte möglichst flexibel von einer Weichensteuerung (zwei weitere RCXe) kontrolliert werden. Als Zusatzaufgabe soll es einem Zug auch erlaubt sein innerhalb des kritischen Bereichs seine Fahrtrichtung zu wechseln, wobei er das Signal dazu von einer Fernbedienung erhält. Es wurde folgendes Schema konstruiert:

An den grünen Punkten werden Touchsensoren am Zug ausgelöst, woraufhin dieser langsam abbremst und vor den Signalen der Weichensteuerung (rote Punkte) zum Stehen kommt (der Weg vom Touchsensor zum Signal wird mittels eines Rotationssensors bestimmt). Wird das Signal von der Weichensteuerung aktiviert, registriert dies ein Lichtsensor am Zug und er fährt in den kritischen Bereich ein. An den blau markierten Stellen werden Touchsensoren vom vorbeifahrenden Zug aktiviert und von der Weichensteuerung registriert. Damit kann festgestellt werden, wo sich welcher Zug befindet. Da beide Weichensteuerungen dies wissen müssen, findet eine Infrarot-Kommunikation ("IR"-Bereich) zwischen den beiden RCXen statt. Damit konnten alle LegOS-Kenntnisse aus den vorherigen Übungen in diesem Projekt angewandt werden.

Schienensystem I

Schienensystem II

Schienensystem III

Die ersten größeren Hürden traten bereits bei der Konstruktion der Hardware aus Lego-Teilen auf. Während die Gleissteuerung recht schnell gebaut werden konnte, musste für die Züge viel ausprobiert werden. Da die RCXe recht schwer sind, musste die Kraft der Motoren sehr effizient auf die Wagenräder übertragen werden. Dadurch war es notwendig, die Antriebseinheit durch viele Querstreben zu festigen. Allerdings durfte dadurch der Zug weder zu breit (der Abstand zwischen den Schienen war relativ klein) noch zu hoch (der Zug würde in den Kurven umkippen) werden. Danach galt es die Sensoren entlang der Schienen zu konstruieren. Als wesentliches Hilfsmittel kamen Gummibänder zum Einsatz. Sie werden durch einen Arm gespannt, welcher vom vorbeifahrenden Zug bewegt wird, und drücken dann ein Lego-Element gegen den Touchsensor. Ähnlich funktioniert der Touchsensor am Zug selbst.

Weichenansteuerung

Touchsensor (

)

Zug-Antriebssystem

Als weitere Aufgabe galt es die entwickelten Programme mittels Uppaal zu verifizieren. Die Steuerung der Züge wurde direkt in C entwickelt, dh. es musste auch der Uppaal-Input manuell geschrieben werden. Die Weichensteuerung hingegen wurde mit Moby/PLC erstellt. Der generierte Uppaal-Code konnte trotz seiner Komplexität mit Hilfe von sicheren Abstraktionen vollständig verifiziert werden. Hierbei kam sehr deutlich der Realzeitaspekt zum Tragen: Aufgrund der Konstruktion werden die Touchsensoren nur sehr kurz ausgelöst, die RCXen der Weichensteuerung haben jedoch (bedingt durch die IR-Kommunikation) eine Zykluszeit von 600ms. Dadurch kann es vorkommen, dass ein vorbeifahrender Zug nicht immer von der Weichensteuerung "gesehen" wird. Erkennt die Steuerung durch später stattfindene Zugbewegungen jedoch, dass so ein Phänomen stattgefunden hat, so wird ein Fehlerzustand angenommen.