Ludwig-Maximilians-Universität München, Institut für Informatik,
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

DAAD/ARC Projekt

Räumlich-zeitliche Logiken für mobile Systeme

Das Internet stellt nicht nur eine globale Infrastruktur zum Austausch von statischen Dokumenten dar, sondern kann auch als Plattform für (weiträumig) verteilte Anwendungen genutzt werden. Diese Entwicklung wird durch die zunehmende Verbreitung mobiler Endgeräte verstärkt, bei denen die Nutzung kompletter Arbeitsumgebungen über administrative und räumliche Grenzen hinweg angestrebt wird. Diese Anwendungen stellen jedoch neue Anforderungen bezüglich der Sicherheit, der Fehlertoleranz und der Verfügbarkeit von Rechen- und Übertragungskapazität, so dass existierende Modelle für lokal verteilte Anwendungen nicht unmittelbar anwendbar sind. Das Ziel dieses Projekts ist es, zur Entwicklung formaler Semantiken und Logiken zur Beschreibung mobiler Systeme beizutragen.

Um Programmiermodelle für mobile Anwendungen fundiert zu entwickeln, müssen die genannten Anforderungen konzeptuell wohl verstanden und in grundlegenden Kalkülen und Beschreibungsmethoden berücksichtigt werden. Die Entwicklung entsprechender formaler Modelle und Theorien steht bisher noch am Anfang, wenn auch in den letzten Jahren einige Kalküle zur Beschreibung mobiler Systeme entwickelt wurden.

Der historisch erste Ansatz zur Formalisierung von Mobilitätsaspekten ist Milners pi-Kalkül, der die Prozessalgebra CCS um das Erzeugen und Versenden von Namen erweitert. Mobilität von aktivem Code wird dagegen im pi-Kalkül nicht direkt unterstützt. Der bekannteste Kalkül zur Modellierung dieser Art von Mobilität ist der Ambient-Kalkül von Cardelli und Gordon, der auch als Ausgangspunkt unserer Arbeiten dient.

In diesem Projekt werden Formalismen und Techniken zur Spezifikation mobiler Systeme auf der Basis geeigneter semantischer Modelle entwickelt, die auf Transitionssystemen beruhen, wobei die räumliche Verteilungsstruktur durch Modellierung der Zustände als Bäume oder Graphen widergegeben wird. Koalgebraische Beschreibungstechniken stellen einen attraktiven Rahmen zur Spezifikation konkreter Transitionssysteme dar und erlauben Bisimulationsrelationen in einem allgemeinen, kategoriellen Ansatz zu charakterisieren und systematisch ausdrucksvollständige Modallogiken zu definieren. Dieser allgemeine Rahmen soll für die spezielle Anwendung auf mobile Systeme instanziiert und (z.B. um Fixpunkt-Operatoren) erweitert werden.

Ferner soll eine geeignete Logik mit räumlichen und zeitlichen Modalitäten entwickelt werden, in der mobile Systeme spezifiziert und ihre Eigenschaften bewiesen werden können. Die Semantik dieser Logik wird auf dem oben genannten Modellbegriff der verallgemeinerten Transitionssysteme beruhen. Die Untersuchung von Meta-Eigenschaften wie Axiomatisierbarkeit und Ausdrucksmächtigkeit (des aussagenlogischen Fragments) wird Aufschluss über die Stärke des Formalismus geben.

Schließlich werden wir Verfeinerungsbeziehungen zwischen mobilen Systemen studieren. Als erster Ausgangspunkt dient der Verfeinerungsbegriff in der Temporallogik TLA. Interessant ist allerdings die Erweiterung dieses Begriffs um die Berücksichtigung der räumlichen Struktur, woraus sich (unter gewissen Bedingungen) neue Verfeinerungskonzepte ergeben können, wie etwa die Spezialisierung administrativer Domänen. Die zuvor entwickelte Logik soll den Nachweis von Verfeinerungsbeziehungen unterstützen.

Projektpartner: Dr. Bernhard Reus, University of Sussex, Brighton, UK

Ansprechpartner: Dr. Stephan Merz, Dr. Dirk Pattinson, Júlia Zappe.