Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

PG 516: A4 - Advanced Automatic Analysis with Automata

 

Thema

Im Rahmen der Projektgruppe AAA (Triple-A) entstand im Sommersemester 2005 und Wintersemester 2005/2006 ein Baukasten zur Programmierung und zum Experimentieren mit automatischen Analyseverfahren, die auf dem Rechnen mit Automaten basieren. Der hier entstandene Baukasten integriert bereits ein Basispaket verschiedener Automatenbibliotheken und Anwendungen und stellt eine leistungsfähige GUI zur Verfügung. Damit eröffnen sich zahlreiche Anwendungsfelder in Forschung und Lehre. Der Baukasten wurde inzwischen der Öffentlichkeit als Open-Source Projekt zugänglich gemacht. Die Projektgruppe AAAA soll den Baukasten in vielerlei Hinsicht erweitern. Mögliche Zielrichtungen hierfür sind die Bereitstellung weiterer Automatenbibliotheken und weiterer Anwendungen, die Weiterentwicklung der GUI  und die Nutzung von Synergieeffekten durch die Anbindung an die jABC-Plattform.

 

Motivation

Bei der automatischen Analyse und Verifikation von Systemen gibt es zahlreiche Anwendungen, in denen Automaten eine Rolle spielen. Dabei 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. Lassen sich die Objekte, an denen man interessiert ist, nämlich als Worte über einem geeignet gewählten Alphabet repräsentieren, so kann ein Automat über diesem Alphabet dann als Repräsentation regulärer Mengen dieser Objekte benutzt werden. Zum Rechnen mit derartig durch Automaten repräsentierten Mengen benutzt man dann einerseits die klassischen Sprachoperationen, Schnitt, Vereinigung, Komplement, aber  auch speziell für die jeweilige Anwendung entwickelte Operationen auf den Automaten.

Beispiele für durch Automaten modellierbare Objekte sind:

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, wobei das  i-tes  Bit  genau dann 1 ist, wenn die Zahl i in der Menge enthalten ist.

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 [6] und zum Teil auch schon in existierenden Analysetools verwendet, z.B. zum Entscheiden der Gültigkeit von Formeln der sogenannten Presburger-Logik [9] und der (schwachen) monadischen Logik zweiter Stufe [4, 8], zur Analyse von Systemen mit unzuverlässigen Kanälen, die Werte verlieren können, (lossy channel systems) [2], zur Analyse von Pointer- und Heapstrukturen [5] und zu Erreichbarkeitsanalysen von Stackautomaten [3].

Das Potential dieses Automatenansatzes zur Analyse erhöht sich noch einmal beträchtlich, wenn auch Automatenklassen betrachtet werden, die über die  klassischen endlichen Automaten hinausgehen. Dabei bieten sich insbesondere an: 

· Baumautomaten: Automaten dieses Typs erkennen anstelle regulärer    Mengen von Wörtern reguläre Mengen von Bäumen (deren Knoten mit Alphabetssymbolen benannt sind)

· w-Automaten Automaten dieses Typs akzeptieren im Gegensatz zu den endlichen Automaten  unendliche Wörter

· Alternierende Automaten: Automaten diesen Typs erlauben Zustandsübergänge mit existenziellen und universellen Bestandteilen.

Auch Kombinationen dieser Automatenklassen sind möglich.

5.2  Erreichter Stand der  PG AAA

Ziel der Projektgruppe AAA (Triple-A), die im Sommersemester 2005 und Wintersemester 2005/2006 stattfand, war 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. Zum anderen wendet es sich an Toolnutzer, die Automaten-basierte Analyseverfahren verwenden oder ausprobieren wollen. Der Automatenbaukasten kann insbesondere auch hervorragend in der Lehre bei der Vermittlung derartiger Verfahren verwendet werden.

Der im Rahmen der PG AAA entstandene Baukasten integriert bereits ein Basispaket verschiedener Automatenbibliotheken. So wurden Java-Bibliotheken mit erheblichem Funktionsumfang für endliche Automaten, Büchi-Automaten und BDDs geschrieben. Auf  Seiten der Anwendungen ist ein Verfahren zum Überprüfen  von Formeln in Presburger Logik und ein Verfahren zum Modelchecking von LTL-Formeln implementiert worden. Darüber hinaus steht eine leistungsfähige GUI zur Verfügung, die es erlaubt Automaten zu visualisieren, Formeln einzugeben und Operationen auf Automaten interaktiv durchzuführen. Der Baukasten wurde inzwischen der Öffentlichkeit als Open-Source-Projekt zugänglich gemacht.

 

Ziele

  • Bereitstellung weiterer Automatenbibliotheken
  • Bereitstellungen weiterer Anwendungen
  • Weiterentwicklung der GUI
  • Nutzung von Synergieeffekten durch die Anbindung an die jABC-Plattform.

 

Teilnahmevoraussetzungen

Erforderlich

  • Kenntnisse mindestens einer objektorientierten Programmiersprache, vorzugsweise Java.
  • Erfolgreiche Teilnahme an der Vorlesung Grundbegriffe der Theoretischen Informatik.
  • Kenntnisse in automatischer Analyse nachgewiesen durch erfolgreiche Teilnahme (zu Beginn SS 07) an einer Vorlesung aus einem der Gebiete Übersetzerbau, Programmanalyse, Verteilte oder parallele Systeme, Theorie der Programmierung oder Formale Methoden des Systementwurfs, SOS und Views.

Wünschenswert

  • Grundkenntnisse in der Programmierung graphischer Oberflächen.

 

Zeitraum

Sommersemester 2007 und Wintersemester 2007/2008

 

Umfang

Jeweils 8 Semesterwochenstunden

 

Veranstalter

  • Ruething

 

Literatur zur Projektgruppe

[1]   Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. A Survey of Regular Model Checking. In Proc. 15th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, 2004. Springer-Verlag.

[2] Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In CAV ’98: Proceedings of the 10th International Conference on Computer Aided Verification, pages 305–318, London, UK, 1998. Springer-Verlag.

 [3] Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR ’97: Proceedings of the 8th International Conference on Concurrency Theory, pages 135–150, London, UK, 1997. Springer-Verlag.

[4] P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. Mosel: A flexible toolset for monadic second-order logic. In Proc. of the Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), Enschede (NL), volume 1217 of Lecture Notes in Computer Science (LNCS), pages 183–202, Heidelberg, Germany, March 1997. Springer-Verlag.

[5] J. R. Larus and P. N. Hilfinger. Detecting conflicts between structure accesses. In PLDI ’88: Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, pages 24–31, New York, NY, USA, 1988. ACM Press.

[6] Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. 10th International Conference on Computer-Aided Verification, number 1427 in LNCS, pages 88–97. Springer-Verlag, 1998.

[7] jABC Website. http://jabc.cs.uni-dortmund.de.

[8] The MONA Project Website. http://www.brics.dk/mona.

[9] The Liège Automata-based Symbolic Handler (LASH). http://www.montefiore.ulg.ac.be/boigelot/research/lash



Nebeninhalt

 

Kontakt

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