Ziele und Resultate

Das Verisoft Projekt ist ein langfristiges Forschungsprojekt, das vom Bundesministerium für Bildung und Forschung (bmb+f) gefördert wird. Verisoft zielt darauf ab, fünf konkrete Anwendungsszenarien zu verifizieren, und zwar eines aus dem akademischen Bereich und vier mit industriellem Hintergrund. Es handelt sich um formale und durchgängige Verifikation, das heißt, computergestützte Verifikationswerkzeuge werden durch alle Abstraktionsschichten verwendet. Auf diese Weise werden menschliche Fehler ausgeschlossen, vollständige Abdeckung wird erreicht und die Ergebnisse basieren auf einem wohlbekannten kleinen Satz von Axiomen. Deshalb weisen die verifizierten Systeme eine extrem hohe Qualität auf, wie sie in vielen Sparten der Industrie gefordert wird, beispielsweise Automotive, Sicherheit und medizinische Technologie. Zusätzlich wird erwartet, dass die Produktivität durch all diejeigen Werkzeuge steigt, die speziell für diese Aufgabe entwickelt oder verbessert werden.

Nachfolgend geben wir eine detaillierte Übersicht über die Ziele und aktuellen Resultate von Verisoft für die einzelnen Teilprojekte. Darüberhinaus finden Sie auf der Verisoft Repository Seite Teile der in Verisoft erzielten Resultate, die hinreichend stabil sind und keine vertraulichen Daten der Industriepartner enthalten.

Teilprojekt 1: Werkzeuge und Methoden

Im TP 1 sollen die Werkzeuge und Methoden (weiter-) entwickelt werden, mit denen die Verifikationsaufgaben aus den Teilprojekten 2, 3, 4 und 6 bewältigt werden sollen. Ferner werden mathematische Grundlagenlücken formal geschlossen.

Teilprojektleiter: (Universität Freiburg); (DFKI)

Teilprojekt 2: Akademisches System

Im TP 2 soll ein durchgehend verifiziertes System zur Übertragung von signierten E-Mails konstruiert werden. Dieses System soll dabei so nahe an tatsächlich verwendeten Lösungen angelehnt sein, dass es als Beispiel für eine reale Anwendung dienen kann. Die zu verifizierenden Eigenschaften des so konstruierten Systems entsprechen dabei den gewünschten Anforderungen an reale Systeme.

Teilprojektleiter: (Universität Koblenz)

Teilprojekt 3: Korrektes industrielles Hardware/Software-System

Im TP 3 soll sowohl die Hardware eines 32bit-Microcontrollers als auch ein repräsentativer Teil der Software und Systemstruktur eines 'System-on-Chip' (SoC) aus dem Mobiltelefonbereich verifiziert werden. Aus Gründen der Vertraulichkeit können wir keine Einzelheiten zu diesem Teilprojekt veröffentlichen.

Teilprojektleiter: Prof. Dr. Wolfram Büttner, OneSpin Solutions

Teilprojekt 4: Biometrisches Identifikationssystem

Im TP 4 soll eine Zugangslösung bestehend aus einem biometrischen Identifikationssystem mit Referenzdatenabspeicherung auf einer Smartcard möglichst durchgängig verifiziert werden.

Teilprojektleiter: (T-Systems)

Teilprojekt 5: Projektmanagement

Im TP 5 werden gesamtprojektrelevante Vorgänge bearbeitet, die wissenschaftliche Arbeit wird koordiniert, Richtlinien für die Zusammenarbeit und den Informationsaustausch werden erarbeitet und die fachliche Abstimmung mit dem bmb+f und dem Projektträger wird wahrgenommen.

Teilprojektleiter: (Universität Saarbrücken)

Teilprojekt 6: Automotive

Im TP 6 soll eine Anwendung aus dem Bereich Automotive durchgehend verifiziert werden. Es handelt sich dabei um den automatischen Automobilnotruf eCall, der nach Auftreten eines Unfalls die Rettungsleitstelle kontaktiert und ihr die Fahrzeugkoordinaten übermittelt. Um die korrekte Funktionsfähigkeit dieses verteilten Systems nachzuweisen, müssen neben der Anwendung eCall auch das Echtzeitbetriebssystem und der Kommunikationsbus betrachtet werden.

Teilprojektleiter: (Technische Universität München)

 
Revision 14 Dec 2006