----------------------------------------------------------------
Projektgruppe "Kooperierende autonome Systeme"
----------------------------------------------------------------

1. Formalia

Bei erfolgreicher Teilnahme an der Projektgruppe wird ein 
PG-Schein f"ur die Theoretische Informatik ausgestellt.

1.1 Veranstalter

Prof. Dr. Ernst-R"udiger Olderog
Dipl.-Inform. Jochen Hoenicke
N.N.

unter Mitarbeit von Dr. Henning Dierks 

1.2 Zeitraum

WS 2001/2002 und SoSe 2002

1.3 Umfang

In beiden Semestern jeweils 8 SWS

1.4 Lehrveranstaltungs"aquivalent 

- 1 Seminar
- 1 Fortgeschrittenenpraktikum
- 1 Sudienarbeit

1.5 Inanspruchnahme von Fachbereichsressourcen

Der Rechner- und Softwarebedarf wird durch Ressourcen der
veranstaltenden Abteilung gedeckt. Als Raum f"ur Sitzungen 
ist der A3 2-214 oder der A3 2-209 vorgesehen.

1.6 Teilnahmevoraussetzungen

Abgeschlossenes Grundstudium mit erfolgreich abgeschlossenem Vordiplom
zu Beginn des WS 2001/2002.


2. Aufgabenstellung

2.1 Zielsetzung

Viele Aufgaben lassen sich besser l"osen, wenn sie auf viele
mitdenkende K"opfe verteilt werden k"onnen. Diese allt"agliche Erfahrung
setzt sich auch bei der industriellen Herstellung von G"utern durch.
Statt einer starren Produktion am Fliessband, bei der die gesamte
Produktion still steht, wenn eine Maschine ausf"allt, wird mit flexibleren
Anordnungen experimentiert, bei der dann eine andere Maschine einspringt
und mit den anderen kooperiert. Dieser Anwendungsbereich geh"ort zum 
Thema "kooperierende autonome Roboter" [1] oder auch "mobile Roboter" [2].
In der Projektgruppe soll ein Schritt in Richung formale Behandlung
von Systemen aus solchen Robotern gemacht weren.

F"ur ein Forschungsprogramm der Deutschen Forschungsgemeinschaft (DFG)
hat das Fraunhofer-Institut f"ur Produktionstechnik und Automatisierung in 
Stuttgart eine sehr attraktive, realistische Fallstudie [3] entwickelt, an 
der mehrere Werkzeugmaschinen, fahrerlose Transportfahrzeuge und
Lager miteinander kooperieren, um Werkst"ucke geeignet zu bearbeiten. 
Dabei k"onnen die Transportfahrzeuge von den Werkzeugmaschinen nach Bedarf 
wie Taxis gerufen werden, um Werkzeugteile zu bringen oder abzuholen.

In der Projektgruppe soll diese Fallstudie in einer gewissen Ausbaustufe
(z.B. drei Werkzeugmaschinen und drei Transportfahrzeuge) spezifiziert,
implementiert und teilweise verifiziert werden. Als Zielhardware sollen
Mini-Roboter eingesetzt werden, die programmierbaren Lego-Mindstorm
Bausteine [4]. Diese besitzen Sensoren und Aktoren zur Kommunikation 
mit ihrer Umwelt, u.a. durch eine Infrarot-Schnittstelle.

Die Implementierung soll durch eine geeignete "Ubersetzung aus der 
Spezifikation gewonnen werden. Dazu soll die in der Abteilung Semantik
entstandene Werkzeugumgebung MOBY/PLC [6] f"ur die Spezifikation und Analyse
von Realzeitsystemen erweitert werden. Bisher k"onnen mit MOBY/PLC nur
Systeme spezifiziert und implementiert werden, deren Komponenten fest
vorgegebene sich auf "fest vorgegebenen Bahnen" bewegen wie es zum Beispiel 
bei einer Eisenbahnsteuerung ausreicht [7].

2.2 Aufgaben

- Entwicklung einer Spezifikationssprache SR mit 
  anwendungsspezifischen Sprachelementen zur Verhaltensbeschreibung
  des Robotersystems,

- Entwicklung eines graphischen Editors f"ur SR und eines
  "Ubersetzers von SR in die Programmiersprache der Lego-Mindstorms 
  als Erweiterung der MOBY-Werkzeugumgebung,

- Entwicklung einer Methodik zur Verifikation von 
  Verhaltenseigenschaften der Roboter durch den Einsatz
  von automatischen Verfahren (Model-Checker)

2.3 Entwicklungsumgebung

  Die Spezifikationssprache und der zugeh"orige "Ubersetzer soll
  in die MOBY-Werkzeugumgebung eingepasst werden.

  Die Implementierungsaufgaben k"onnen an den Rechnern der Abteilung
  durchgef"uhrt werden.

  Die MOBY-Werkzeugumgebung ist in C++ geschrieben und l"auft unter
  Solaris und Linux. Zur Versionskontrolle wird CVS eingesetzt. Die
  Dokumentation soll mit LaTeX geschrieben werden. Die Lego-Roboter
  werden in normalem C oder C++ programmiert und laufen unter dem
  speziellem Minimal-Betriebssystem legOS [5].

2.4 Minimalanforderungen f"ur die Teilnahme

- Aktive Mitarbeit bei der Analyse, Konzeption und Implementierung
- Erf"ullung "ubertragener Aufgaben
- Pr"asentation und Ausarbeitung von Seminarvortr"agen
- Erstellung von Zwischen- und Endbericht sowie anfallenden Dokumentationen

2.5 Zeitplanung

WS 2001/2002:
 - Seminarphase
 - Einarbeitung in Lego Mindstorm Roboter, Fallstudie, MOBY/PLC 
 - Analyse der Fallstudie
 - Entwicklung der Spezifikationssprache SR
 - Konzeption des Editor fuer SR
 - Konzeption der "Ubersetzung von SR in die Lego Mindstorms
 - Konzeption einer Methodik zur Verifikation
 
Vorlesungsfreie Zeit nach dem Ende des WS 2001/2002:
 - Anfertigung des Zwischenberichts

SoSe 2002:
 - Einarbeitung in das automatische Verifizieren
 - Entwicklung des Editors
 - Entwicklung des "Ubersetzers
 - Teilweise Verifikation

Vorlesungsfreie Zeit nach dem Ende des SoSe 2002:
 - Anfertigung des Endberichts
 - Fertigstellung der Dokumentation
 - Abschlusspr"asentation

3. Literatur

Zum Vorhaben der Projektgruppe sind die Ausgangsinformationen
wie folgt im Internet zu finden:

[1] Ein Projekt namens "Cooperating Autonomous Robots":

    http://www.epm.ornl.gov/cap.html

[2] Links zum Thema mobile Roboter:

    http://www-robotics.usc.edu/~gaurav/DARPA_mobile.html
    http://robby.caltech.edu/~choset/mobile_robot.html

[3] DFG-SPP "Integration von Spezifikationstechniken f"ur 
    ingenieurwissenschaftliche Anwendungen":
   
    http://tfs.cs.tu-berlin.de/projekte/indspec/SPP

[4] Lego Mindstorm Roboter:

    http://mindstorms.lego.com

[5] Die legOS Homepage:

    http://legos.sourceforge.net/

[6] MOBY/PLC Werkzeugumgebung:

    http://semantik.informatik.uni-oldenburg.de/projects/mobyplc.html

[7] Ergebnisbericht des F-Praktikums "Realzeitsysteme" im WS 2000/2001:
 
    http://semantik.informatik.Uni-Oldenburg.DE/teaching/fp_realzeitsys_ws0001/result