Aktuelle Projekte

Forschungsgebiet unserer Gruppe sind formale, logikbasierte Methoden zur Spezifikation, Verifikation und Analyse von Software. Ziel ist es, die Verlässlichkeit und Sicherheit kritischer Systeme zu erhöhen.

Neben Methoden zur Verifikation funktionaler Korrektheit werden - insbesondere für Anwendungen in der IT-Sicherheit - Methoden zum Nachweis von Informationsflusseigenschaften entwickelt. Zu den betrachteten Praxisszenarien gehören diverse Anwendungen wie objekt-orientierte Software, Software zur Steuerung von Industrie-Anlagen und elektronische Wahlsysteme.


COST Action IC1205: COMSOC

Rechenbetonte Sozialwahltheorie

Die rechenbetonte Sozialwahltheorie (Computational Social Choice) ist ein sich rapide weiterentwickelnder Forschungszweig, der sich mit dem Design und der Analyse von Methoden der kollektiven Entscheidungsfindung beschäftigt. Er kombiniert Methoden der Informatik mit Erkenntnissen der Wirtschaftstheorie. Die COST Action IC1205 zu Computational Social Choice ist ein europäisches Forschungsnetzwerk, das aufgebaut wurde, um eine gemeinsame Plattform zur Forschung in diesem Feld europaübergreifend und darüber hinaus herzustellen.

Innerhalb dieses Projekts konzentrieren wir uns auf die Spezifikation und Verifikation von Wahlverfahren. Ein Wahlverfahren, als eine Methode individuelle Präferenzen zu einer aggregierten Wahlentscheidung zu kombinieren, ist Teil des grundsätzlichen demokratischen Verfahrens. Es ist also unerlässlich, dass Wahlverfahren wie vorgesehen funktionieren. Das Ziel des Projektes ist die Entwicklung formaler Verifikationstechniken, die es erlauben, Eigenschaften von Wahlverfahren ohne den riesigen Overhead einer für eine voll-funktionale Verifikation notwendigen Nutzer-Interaktion zu überprüfen. Die resultierende Methodik könnte dann in einem iterativen Design- und Implementierungsprozess neuer Wahlverfahren eingesetzt werden.

COST Action

DeduSec

Spezifikation und Deduktive Verifikation von Sicherheitseigenschaften auf Programmebene

In den letzten Jahren wurde ein deutlicher Fortschritt in der formalen Verifikation funktionaler Eigenschaften von Programmen erzielt. Gleichzeitig wurden zukunftsweisende Papiere veröffentlicht, die zeigen, dass es grundsätzlich möglich ist, Informationsfluss-Eigenschaften als Beweisverpflichtungen in Programm-Logik zu formulieren.

Das Gesamtziel des Projektes ist es diese Fortschritte — zusammen mit unseren eigenen Erfahrungen im Bereich der formalen Methoden für funktionale Eigenschaften — einzusetzen um Sicherheitseigenschaften zu spezifizieren und verifizieren.

DeduSec Projekt

Software Campus Projekt: FIfAKS

Formale Informations-Flußanalyse für komponenten-basierte Systeme

Ziel des Software Campus Programmes ist es, die IT-Führungskräfte von morgen auszubilden. Die Projekte im Rahmen des Software Campus werden in Kooperation mit einem Forschungspartner und einem Industriepartner durchgeführt.

Das Projekt "Formale Informations-Fluss Analyse für komponenten-basierte Systeme" ist ein Projekt in Zusammenarbeit mit DHL IT-Services in Bonn.

Das Ziel ist es, Sicherheitsanalysen von komponenten-basierten Systemenwährend des System-Designs durchzuführen.

FIfAKS Projekt

IMPROVE APS

Regression Verification in einem Nutzer-zentrierten Softwareentwicklungs-Prozess für sich kontinuierlich entwickelnde automatisierte Produktionsanlagen

Die Vision dieses Projektes besteht darin, die Technologie voranzubringen, sodass Methodiken der Regression Verification verfügbar sind, die routinemäßig verwendet werden, Korrektheit im Evolutionsprozess langlebiger verlässlicher Systeme, die eine regelmäßige Re-Validierung erfordern, zu garantieren. Das Ziel von Regression Verification ist es, formal zu beweisen, dass die Korrektheit von Software während ihres Evolutionsprozesses erhalten bleibt, Änderungen den gewünschten Effekt haben, und keine neuen Bugs eingeführt werden.

Regression Verification umgeht den Haupt-Flaschenhals zur routinemäßigen praktischen Verwendung formaler Verifikation, nämlich die Notwendigkeit voll-funktionale Spezifikationen zu schreiben (was einen enormen Aufwand darstellt). Außerdem, gegeben zwei gleichermaßen komplexe aber ähnliche Programm-Versionen oder -Varianten, hängt der Aufwand, den Zusammenhang zwischen ihnen zu verifizieren, hauptsächlich vom Unterschied zwischen den Programmen und nicht von ihrer gesamten Größe und Komplexität ab.

IMPROVE-APS Projekt

KASTEL

Intelligente Infrastrukturen, Cloud Computing und öffentliche Sicherheit stellen große Herausforderungen an die IT-Sicherheit der Zukunft. Zusätzlich zum klassischen Schutz der Peripherie muss mit Bedrohungen von innen umgegangen werden. Es genügt nicht mehr, die Sicherheit von Teilsystemen zu betrachten. Dabei bedarf es disziplinenübergreifender Methoden. Das Kompetenzzentrum für Angewandte Sicherheits-TEchnoLogie (KASTEL) bündelt die Kompetenzen verschiedener Teildisziplinen der IT-Sicherheit und der Anwender.

KASTEL Projekt

KeY

Integriertes Deduktives Software-Design

Das KeY-System ist ein Werkzeug zur formalen Software-Entwicklung, das darauf ausgerichtet ist, Entwurf, Implementierung, formale Spezifikation und formale Verifikation objekt-orientierter Software möglichst nahtlos miteinander zu vereinen. Im Zentrum des Systems steht ein neuartiger Theorembeweiser für dynamische Logik erster Ordnung für Java mit einer anwendungsfreundlichen Oberfläche.

Das Projekt begann im November 1998 an der Universität Karlsruhe. Inzwischen ist es ein gemeinsames Projekt des KIT, Chalmers University of Technology in Göteborg und der TU Darmstadt und wird von der DFG gefördert.

KeY Projekt

Lehre hoch Forschung-PLUS

Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der Informatik

Das Hauptziel des Projekts LehreForschung-PLUS ist die Verbesserung der Studienbedingungen und kontinuierliche Steigerung der Lehrqualität durch eine flächendeckende Weiterentwicklung der Studiengänge.

Unser Teilprojekt umfasst hierbei drei wesentliche Maßnahmen, die alle das Ziel verfolgen, projekt- und forschungsorientierte, sowie interdisziplinäre Lehre in den Informatik-Studiengängen umzusetzen und zu stärken.

Diese beinhalten die Weiterentwicklung und Verbesserung des projekt- und forschungsorientierten Master-Moduls "Praxis der Forschung", des projektorientierten Bachelor-Moduls "Praxis der Softwareentwicklung", sowie die Einführung des interdisziplinären und forschungsorientierten Studienprofils "Internet und Gesellschaft".

Teilprojekt "LehreForschung-PLUS – Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der Informatik"


Abgeschlossene Projekte

COST Action IC0701: Formale Verifikation objekt-orientierter Software

Das Hauptziel dieser "Action" ist, eine Verifikationstechnologie zu entwickeln, die weitreichend und stark genug ist, um die Zuverlässigkeit objekt-orientierter Software in industrieller Größe zu garantieren.

COST steht für "European Cooperation in the Field of Scientific and Technical Research". Es ist ein internationales Netzwerk zur Förderung der Zusammenarbeit europäischer Forscher als Basis. Mehr Information über COST befindet sich auf der allgemeinen COST Webseite. COST ist in "Actions" gegliedert. Das Ziel dieser Action ist, eine Verifikationstechnologie zu entwickeln, die weitreichend und stark genug ist, um die Zuverlässigkeit objekt-orientierter Software in industrieller Größe zu garantieren.

COST Action

GIF: Reliable Software Evolution

In diesem Projekt werden Testverfahren und formale Methoden kombiniert um die Zuverlässigkeit von evolvierender Software zu gewährleisten. Mit dem Fokus auf evolvierende Software behandeln wir eine wichtige Phase im Lebenszyklus eines Softwaresystems und heben die inkrementelle Natur von Softwareänderungen hervor.

GIF Projekt

IMPROVE

Regression Verification für evolvierende objekt-orientierte Software

Das Ziel dieses Projekts ist es, die Fortschritte in der deduktiven Programm-Verifikation zu nutzen, um Regression Verification zu ermöglichen. Mit der Hilfe von Regression Verification ist es möglich zu beweisen, dass  die Korrektheit von Software während ihres Evolutionsprozesses erhalten bleibt und keine neuen Bugs eingeführt werden. In diesem Projekt wird eine Regression Verification Methodik für Java entwickelt, die mächtig genug ist, um auf Beispiele aus der Praxis angewandt zu werden.

IMPROVE Projekt

Integration von Deduktion und Model Checking zur Prüfung systemnaher Software

Die Integration von deduktiver Programmverifikation und Bounded Model Checking (BMC) ist Gegenstand aktueller Arbeiten in Zusammenarbeit mit der Arbeitsgruppe von Dr. C. Sinz

Während die Verfahren zur deduktiven Verifikation neben der Anforderungsspezifikation eines Programms eine Vielzahl an Hilfen durch den Benutzer erfordert (Schleifeninvarianten, Spezifikationen von Hilfsfunctionen etc.), kommt BMC weitgehend ohne solchge Hilfen aus. Der Vorteil von deduktiver Verifikationis ist die höhere Präzision und die ausdrucksstärkeren Spezifikationsprachen.

Ein erstes Ziel der Arbeiten zur Kombination dieser Stärken ist es, BMC dazu einzusetzen, die iterative Interaktion zwischen Benutzer und deduktivem Verifikationswerkzeug zu verbessern: die Anbindung eines BMC-Werkzeugs soll es erlauben, Teile der Spezifikation eines Programms zu überprüfen bevor mit dem deduktiven Beweis begonnen wird.

Lehre hoch Forschung

Problemorientierte Lehre

Das Hauptziel des Projekts "Lehre hoch Forschung" ist die Verbesserung von Studienbedingungen und Lehrqualität, sowie die frühe Einbindung von Forschung in das Bachelor- und Master-Studienprogramm.

Des Weiteren ist es Ziel von „Lehre hoch Forschung“, künftig flächendeckend problemorientierte, forschungsorientierte Praktika und Projekte anzubieten, zu denen Studierende bereits in frühen Fachsemestern Zugang erhalten. Dabei geht es um einen breiten Einblick in relevante Aspekte der Grundlagen- und angewandten Forschung, genauso wie um überfachliche und transdisziplinäre Kompetenzen.

Unsere Arbeitsgruppe ist verantwortlich dafür, das Master-Modul "Praxis der Forschung" zu etablieren und zu koordinieren. Studierende lernen hier, ein Forschungsprojekt durchzuführen: angefangen vom Schreiben des Projektantrags, über die Durchführung des Projekts bis hin zur wissenschaftlichen Publikation der Ergebnisse. Die Projekte behandeln Themen aktueller Forschungsprojekte.

Teilprojekt "Lehre hoch Forschung – Problemorientierte Lehre"

Software Campus Projekt: USV

Usability von Software-Verifikationssystemen: Evaluierung und Verbesserung

Ziel des Software Campus Programmes ist es, die IT-Führungskräfte von morgen auszubilden. Die Projekte im Rahmen des Software Campus werden in Kooperation mit einem Forschungspartner und einem Industriepartner durchgeführt.

Das Projekt "Usability von Software-Verifikationssystemen: Evaluierung und Verbesserung (USV)" ist ein Projekt in Zusammenarbeit mit der DATEV eG in Nürnberg. Das Ziel ist es, die Usability von Software-Verifikationssystemen zu evaluieren und auf der Basis der Evaluationsergebnisse Mechanismen zu entwickeln, um die Produktivität solcher Systeme zu verbessern.

USV Projekt

Verisoft XT

Das zentrale Ziel des Projekts ist die durchdringende (engl. pervasive) formale Verifikation von Computer-Systemen.

Die korrekte Funktionalität von Systemen, wie sie beispielsweise im Automobilbau und Bereich der Sicherheitstechnik verwandt werden, werden formal-mathematisch überprüft.

Szenarios

  • Anwendung im Automobil-Bereich
  • Anwendung im Bereich Avionik
  • Betriebssysteme, Hypervisors

Korrektheitsbeweis eines eingebetteten Betriebssystemkernels

In unserer Forschungsgruppe untersuchen wir schwerpunktmäßig die Spezifikation und Verifikation eines Microkernels mit Partitionierungsschicht, der in der Avionik industriell Einsatz findet.

Dabei verwenden wir das Verifikationstool VCC von Microsoft Research, um funktionale Eigenschaften des von der Firma SYSGO AG entwickelten Kernels PikeOS auf Implementierungsebene zu beweisen.

Verisoft Projekt