Verisoft XT

Moderne Methoden der formalen Verifikation

Kontakt: Prof. Dr. Rolf Drechsler

Softwarefehler verursachen in Europa jährlich einen wirtschaftlichen Schaden von weit über 100 Milliarden Euro. Weil bei der Entwicklung von Software die Anforderungen oft falsch eingeschätzt werden und die existierende Technologie der Fehlersuche sehr aufwändig ist, wenden Hersteller heute 70-80 Prozent ihrer Arbeit für das Entfernen von Softwarefehlern auf. Zuverlässig funktionierende und sichere Software ist aber nicht nur ein Wettbewerbsvorteil für Unternehmen, sondern auch Voraussetzung für sichere Anwendungen etwa im Auto, der Medizin oder Sicherheitstechnik. Das Bundesministerium für Bildung und Forschung (BMBF) fördert daher das Forschungsprojekt VERISOFT XT in den kommenden drei Jahren mit rund 12 Millionen Euro. Ziel ist die Erarbeitung eines Qualitätssiegels "Verified in Germany". Dazu sollen Methoden und Werkzeuge für die formale Verifizierung des Designs von integrierten Computersystemen geschaffen werden. Das bedeutet, den mathematischen und maschinell überprüften Beweis zu erbringen, dass die betrachteten Computersysteme im Entwurf Null Fehler enthalten. Während im Vorläuferprojekt die mathematischen Grundlagen hierfür erarbeitet wurden, geht es bei VERISOFT XT um beispielhafte industrielle Anwendungen. Hierbei müssen Programme mit zehntausenden Zeilen Code verifiziert werden. In dem Projektkonsortium arbeiten zehn Partner aus der Wirtschaft, - kleine und große Unternehmen - sowie sieben Universitäten zusammen. Das Vorhaben wird im Rahmen des BMBF-Programms IKT 2020 - Forschung für Innovationen durchgeführt. Von Seiten der Universität Bremen ist an dem Großprojekt die Arbeitsgruppe Rechnerarchitektur unter der Leitung von Professor Rolf Drechsler beteiligt. Der Forschungsschwerpunkt der Informatiker liegt in der Entwicklung und Anwendung formaler Verifikationstechniken, die die Korrektheit von Schaltungen und Systemen garantieren. Ein Anwendungsbeispiel kommt aus dem Automobilbereich. Ein Fahrzeug enthält heute durchschnittlich 50 Steuergeräte (ABS, EPS etc.) bestehend aus jeweils rund 300 Elektronikbauteilen. Beträgt die Ausfallrate jedes dieser 15.000 Bauteile aufgrund von Produktions-, Entwurfs- oder Betriebsfehlern eins zu einer Million, dann akkumuliert sich dieses scheinbar geringe Risiko zu einer Ausfallrate von 1,5% für die gesamte Elektronik. Bei zu erwartender Verdopplung des Elektronikanteils in Fahrzeugen und Wegfall mechanischer Rückfallebenen verschärft sich dieses Problem entsprechend. In VERISOFT XT soll deshalb die Funktion und das Echtzeitverhalten eines kompletten Mikrokontrollersystems in einem Steuergerät, das eine sicherheitskritische Funktion im Fahrwerk eines Oberklassefahrzeuges implementiert, formal verifiziert werden.