Suche

Unterstützung im Bereich "Formale Methoden"


Formale Methoden dienen dazu, Garantien für die Korrektheit von Systemen (reine Softwaresysteme, aber auch eingebettete Systeme wie z.B. in Autos, Flugzeugen etc.) sicherzustellen. Dies ist aufwändig, und wir beschäftigen uns deshalb mit Anwendungen, die entweder sicherheitskritisch (sowohl im Sinne von Safety: Gefahr von großen Schäden bei Ausfall als auch im Sinne von Security: Schutz vor unerlaubtem Zugriff) oder von wichtiger Bedeutung für die korrekte Funktion vieler Systeme (z.B. Betriebssysteme, Compiler etc.) sind.

Ziel unserer Arbeit ist sowohl die Anwendungen existierender Beweistechniken, als auch die Entwicklung neuer Beweisverfahren (insbesondere bei nebenläufigen Systemen, oder auch bei komplexen Pointer-Strukturen gibt es noch viele ungelöste Probleme, und viele konkurrierende Ansätze).

Zur Anwendung von formalen Methoden setzen wir eine Reihe automatischer Tools ein:

  • Modelchecker wie z.B NuSMV oder, wenn die Wahrscheinlichkeit von Risiken wichtig ist: PRISM .
  • Das Tool Alloy, das sehr effizient Gegenbeispiele für Korrektheitsbehauptungen liefert
  • automatische Beweiser wie z.B. Microsofts Z3
Mögliche Aufgaben für Studenten in diesem Bereich sind die Anwendung derartiger Werkzeuge auf passende Fallstudien. Hierfür sind nur Grundkenntnisse aus der Vorlesung "Logik für Informatiker" notwendig.

Da automatische Techniken bei großen Fallstudien nicht ausreichen, ist unser stärkstes Werkzeug das von uns entwickelte KIV System, das interaktives Beweisen ermöglicht, bei dem der "Beweisingenieur" die entscheidenden Hinweise gibt, wie ein Beweis auszusehen hat.

KIV ist in der Programmiersprache Scala implementiert. Scala ist eine der modernsten Programmiersprachen, die es derzeit gibt. Die Sprache enthält sowohl Weiterentwicklungen objektorientierter Konzepte aus Java, als auch funktionale Konzepte. Die Sprache hat eine Java-ähnliche Syntax und ist zu Java kompatibel, da der Compiler ebenfalls JVM Bytecode erzeugt.

Mögliche Aufgaben für Studenten in diesem Bereich sind die Programmierung verschiedener Aufgaben in Scala. An Vorkenntnissen sind nur Grundkenntnisse in der Programmierung mit Java (typischerweise mit Eclipse) und Interesse an Scala notwendig. Zu diesem Thema gibt es auch Bachelor- und Masterarbeiten. Dort finden sich noch weitere Informationen zu diesem Thema.

An unserem Lehrstuhl finden zwei große Projekte im Bereich "Formale Methoden": statt:

  • Das Projekt VeriCAS beschäftigt sich mit der Verifikation von lockfreien Algorithmen. Diese Algorithmen (Standardalgorithmen findet man inzwischen auch in der Java Library) sind sehr effiziente Lösungen zum nebenläufiigen Zugriff auf Datenstrukturen durch die heute üblichen Multi-Core Prozessoren. Gerade in den letzten Jahren sind eine grosse Zahl neuer Algorithmen entwickelt worden, die wir untersuchen wollen.

  • Das Projekt Flashix zielt auf ein vollständig verifiziertes und lauffähiges Flash Dateisystem ab. Flash-Speicher werden u.a. in Raumfahrzeugen (z.B. Mars Rover) oder Autos eingesetzt.

In diesen Projekten setzen wir hauptsächlich das KIV-System ein. Mögliche Aufgaben für Studenten in diesem Bereich sind die Analyse der zu untersuchenden Algorithmen (für Flashix insbes. das in C programmierte Flash-Dateisystem UBIFS, aus dem Linux-Kernel, fur VeriCAS Algorithmen in verschiedenen Programmiersprachen), sowie die Spezifikation und Verifikation dieser Algorithmen mit KIV. Hierfür sind Vorkenntnisse aus der Vorlesung "Formale Methoden im Software Engineering" wünschenswert.

Weitere Informationen zu Abschlussarbeiten in den einzelnen Themen finden sich hier.

Aktuelle Stellen werden auch auf unseren Pinnwänden am Lehrstuhl ausgeschrieben.

Habt Ihr Interesse?

Dann meldet Euch bei Jörg Pfähler (Flashix) oder Gerhard Schellhorn (Scala, autmatische Techniken).