Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

PG 479: AAA - Automatische Analyse mit Automaten

 

Thema

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.

 

Motivation

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:

  1. Natürliche Zahlen kann man in gewohnter Weise durch ihre Binärdarstellung, ein Wort über dem Alphabet {0; 1}, darstellen.
  2. Endliche Mengen natürlicher Zahlen kann man durch einen Bitstring, ebenfalls ein Wort über dem Alphabet {0; 1}, darstellen.
  3. Den Inhalt eines asynchronen Kommunikationskanals, der die Daten d1; : : : ; dk übertragen kann, kann man durch ein endliches Wort über dem Alphabet {d1; : : : ; dk} repräsentieren.
  4. Den Inhalt eines Stacks kann man durch das Wort der auf dem Stack gespeicherten Symbole repräsentieren.

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.

 

Ziele

 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.

 

Teilnahmevoraussetzungen

Erforderlich

  • Kenntnisse mindestens einer objektorientierten Programmiersprache, vorzugsweise Java.
  • Erfolgreiche Teilnahme an der Vorlesung Grundbegriffe der Theoretischen Informatik.

Wünschenswert

  • Kenntnisse in automatischer Analyse wie sie etwa in Vorlesungen zu den Themengebieten Übersetzerbau, Programmanalyse, Verteilte oder parallele Systeme, Theorie der Programmierung oder Formale Methoden des Systementwurfs vermittelt werden.
  • Grundkenntnisse in der Programmierung graphischer Oberflächen.

 

Zeitraum

Wintersemester 2005/2006 und Sommersemester 2006

 

Umfang

Jeweils 8 Semesterwochenstunden.

 

Veranstalter

  • Dr. Oliver Rüthing
  • Dr. Hubert Wagner


Nebeninhalt

 

Kontakt

Tel. (0231) 755-5801
Fax (0231) 755-5802