Es wird ein Baukasten zur Programmierung und zum Experimentieren mit automatischen Analyseverfahren erstellt, die auf dem Rechnen mit Automaten basieren. Das entwickelte System wendet sich einerseits an Toolnutzer, die Automaten-basierte Analyseverfahren verwenden oder ausprobieren wollen. Es kann somit in der Lehre bei der Vermittlung derartiger Verfahren verwendet werden. Andererseits wendet es sich auch an Toolkonstrukteure, die neue Automaten-basierte Verfahren implementieren oder existierende Verfahren in neuartiger Weise kombinieren wollen. Somit hat das System auch Anwendungen in der Forschung.
Jeder Informatikstudent lernt in den Theorievorlesungen der ersten Semester endliche Automaten als Akzeptoren für reguläre Sprachen kennen. Später tauchen Automaten dann wieder in Syntaxanalyseanwendungen auf, z.B. zur Behandlung regulärer Ausdrücke oder beim Erkennen von Token im Compilerbau. Damit erschöpft sich die Anwendbarkeit von Automaten in der Informatik aber keineswegs, es gibt viele weitere Anwendungen. In dieser Projektgruppe wollenwir einen Softwarebaukasten für Anwendungen von Automaten bei der automatischen Analyse und Verifikation von Systemen konstruieren. All diesen Anwendungen gemeinsam ist die zu Grunde liegende Idee, Automaten als eine Datenstruktur zur Repräsentation von und zum Rechnen mit i.A. unendlichen Mengen gewisser Objekte zu benutzen. Dazu überlegt man sich in einem ersten Schritt, wie man die Objekte, an denen man interessiert ist, als Worte über einem geeignet gewählten Alphabet repräsentieren möchte. Ein Automat über diesem Alphabet kann dann als Repräsentation der Menge derjenigen Objekte benutzt werden, deren Repräsentation von dem Automaten erkannt wird. Zum Rechnen mit derartig durch Automaten repräsentierten Mengen benutzt man dann einerseits die klassischen Sprachoperationen, Schnitt , Vereinigung, Komplement etc., denn man weiß ja, dass reguläre Sprachen unter diesen Operationen abgeschlossen sind, und weiß auch, wie man sie für Automaten berechnet. Andererseits benutzt man speziell für die jeweilige Anwendung entwickelte Operationen auf den Automaten. Da man ganz verschiedene Arten von Objekten adäquat durch Wörter über einem geeigneten Alphabet beschreiben kann, hat die im vorigen Absatz beschrieben Idee viele verschiedene Anwendungen. Hier sind einige Beispiele:
Derartige Repräsentationen werden in verschiedenen in der Literatur vorgeschlagenen Analyseverfahren [5] und zum Teil auch schon in existierenden Analysetools verwendet, z.B. zum Entscheiden der Gültigkeit von Formeln der sogenannten Presburger-Logik [8] und der (schwachen) monadischen Logik zweiter Stufe [3, 7], zur Analyse von Systemen mit unzuverlässigen Kanälen, die Werte verlieren können, (lossy channel systems) [1], zur Analyse von Pointerund Heapstrukturen [4] und zu Erreichbarkeitsanalysen von Stackautomaten [2].
Benutzt man anstelle von Automaten über Wörtern sog. Baumautomaten, die anstatt regulärer Mengen vonWörtern reguläre Mengen von Bäumen (deren Knoten mit Alphabetssymbolen benannt sind) erkennen, erweitert sich die Anwendbarkeit dieses Automatenansatzes zur Analyse noch einmal beträchtlich. Weiterhin kann man Automaten verwenden, die unendlicheWörter akzeptieren.
Ziel der Projektgruppe ist es, einen Baukasten zur Programmierung und zum Experimentieren mit automatischen Analyseverfahren zu erstellen, die auf dem Rechnen mit Automaten basieren. Das entwickelte System wendet sich zum einen an Toolkonstrukteure, die neue oder bekannte Automaten-basierte Verfahren implementieren wollen oder existierende Verfahren in neuartiger Weise kombinieren wollen. Somit hat das System Anwendungen in der Forschung. Zum anderen wendet es sich an Toolnutzer, die Automaten-basierte Analyseverfahren verwenden oder ausprobieren wollen. Es kann somit auch in der Lehre bei der Vermittlung derartiger Verfahren verwendet werden. Zur Verwendung durch Toolkonstrukteure soll eine Java-Bibliothek erstellt werden, die es erlaubt, Automaten als Datenstruktur in verschiedensten Anwendungen zu verwenden, ggf. als Erweiterung einer existierenden Automatenbibliothek wie z.B. dk.brics.automaton
Ziel der Projektgruppe ist es, einen Baukasten zur Programmierung und zum Experimentieren mit automatischen Analyseverfahren zu erstellen, die auf dem Rechnen mit Automaten basieren. Das entwickelte System wendet sich zum einen an Toolkonstrukteure, die neue oder bekannte Automaten-basierte Verfahren implementieren wollen oder existierende Verfahren in neuartiger Weise kombinieren wollen. Somit hat das System Anwendungen in der Forschung. Zum anderen wendet es sich an Toolnutzer, die Automaten-basierte Analyseverfahren verwenden oder ausprobieren wollen. Es kann somit auch in der Lehre bei der Vermittlung derartiger Verfahren verwendet werden. Zur Verwendung durch Toolkonstrukteure soll eine Java-Bibliothek erstellt werden, die es erlaubt, Automaten als Datenstruktur in verschiedensten Anwendungen zu verwenden, ggf. als Erweiterung einer existierenden Automatenbibliothek wie z.B. dk.brics.automaton [9]. Eine wichtige Teilaufgabe ist dabei die Festlegung einer geeigneten Schnittstelle, die einerseits hinreichende Kapselung der Implementierungsdetails erlaubt, andererseits aber exibel genug ist, um in den intendierten Anwendungsszenarien zur Implementierung der verschiedenen Verfahren benutzbar zu sein. Um die Festlegung der Schnittstelle vorzubereiten, soll in einer Seminarphase zu Beginn der Projektgruppe von den Teilnehmern zunächst ein Überblick über existierende Verfahren anhand von Originalliteratur erarbeitet werden. Sowohl zur Verwendung durch Toolnutzer als auch zur Validierung der Automatenbibliothek soll darüber hinaus eine Reihe von Analyseverfahren mit Hilfe der entwickelten Automatenbibliothek implementiert und Benutzern in einer graphischen Benutzerober äche zur Verfügung gestellt werden. Diese graphische Benutzerober äche könnte etwa durch Integration in die schon seit längerem am Lehrstuhl 5 entwickelte jABC-Toolumgebung konstruiert werden.
Eine wichtige Teilaufgabe ist dabei die Festlegung einer geeigneten Schnittstelle, die einerseits hinreichende Kapselung der Implementierungsdetails erlaubt, andererseits aber flexibel genug ist, um in den intendierten Anwendungsszenarien zur Implementierung der verschiedenen Verfahren benutzbar zu sein. Um die Festlegung der Schnittstelle vorzubereiten, soll in einer Seminarphase zu Beginn der Projektgruppe von den Teilnehmern zunächst ein überblick über existierende Verfahren anhand von Originalliteratur erarbeitet werden. Sowohl zur Verwendung durch Toolnutzer als auch zur Validierung der Automatenbibliothek soll darüber hinaus eine Reihe von Analyseverfahren mit Hilfe der entwickelten Automatenbibliothek implementiert und Benutzern in einer graphischen Benutzeroberfläche zur Verfügung gestellt werden. Diese graphische Benutzeroberfläche könnte etwa durch Integration in die schon seit längerem am Lehrstuhl 5 entwickelte jABC-Toolumgebung konstruiert werden. Erweiterungsmöglichkeiten. In einer ersten Ausbaustufe soll zunächst eine Bibliothek für Automaten, die Sprachen endlicher Wörter erkennen, erstellt werden, wie sie aus den Theorievorlesungen des Grundstudiums bekannt sind. Desweiteren sollen einige darauf basierende Verfahren implementiert und in einer graphischen Benutzeroberfläche zur Verfügung gestellt werden. In späteren Ausbaustufen kann die Bibliothek um weitere Automatentypen ergänzt werden, etwa um Baumautomaten und/oder um Automaten zur Erkennung unendlicher Wörter und Bäume. Außerdem können weitere Analyseverfahren implementiert und in die graphische Benutzeroberfläche integriert werden. Je nach Interesse der Teilnehmer und Fortschritt der Arbeiten können diese Arbeiten entweder in einer späteren Phase der Projektgruppe angegangen werden oder in Folgeprojektgruppen. Denkbar ist auch ein Ausbau des System im Rahmen von Folgeprojekten in Form von Hiwi-Tätigkeiten, Diplomarbeiten oder Dissertationen. Im Laufe der Zeit könnte so eine universelle Platform für Automaten-basierte Analyseverfahren entstehen.
Erforderlich
Wünschenswert
Wintersemester 2005/2006 und Sommersemester 2006
Jeweils 8 Semesterwochenstunden.