BMBF-Forschungsprojekt Verisoft der Saarbrücker Informatik auf der CeBIT

[idw]

CeBIT 2006Fehlerfreie Soft- und Hardwarein Auto-ElektronikInformatiker führen für automatischen Autonotruf eCall den Beweis, dass Soft- und Hardware garantiert keine Entwurfsfehler enthalten - BMBF-Forschungsprojekt Verisoft am CeBIT-Stand des Bundesministeriums für Bildung und ForschungIn Autos wird immer mehr Elektronik eingesetzt, insbesondere auch in sicherheitskritischen Komponenten wie dem Antiblockiersystem (ABS) oder Airbag. Leider ist mit der Anzahl und Komplexität der Komponenten auch die Zahl der Fehler stark gestiegen. Laut ADAC sind ein Drittel aller Autopannen auf Mängel in der Elektronik zurückzuführen, rund 80 Prozent davon sind Softwarefehler. Um die aufwändige und teure Suche nach diesen Fehlern mittels herkömmlicher Tests zu vermeiden, setzen Forscher im Verisoft-Projekt unter Leitung des Saarbrücker Informatik-Professors Wolfgang Paul schon vor der Produktion an. Sie zeigen, dass die Soft- und Hardware im Fahrzeug exakte Vorgaben erfüllen, die zudem in sich schlüssig sind. Damit wird mit mathematischer Präzision nachgewiesen, dass Soft- und Hardware im Fahrzeug keine Entwurfsfehler enthalten. Zur Zeit kann kein Hersteller vergleichbare Sicherheiten garantieren. Um die Machbarkeit ihres Ansatzes zu zeigen, untersuchen die Wissenschaftler ein beispielhaftes, aber dennoch repräsentatives Szenario: eCall ist ein System, das nach einem Unfall automatisch Rettungskräfte alarmiert und dadurch Leben retten kann. eCall soll nach dem Willen der Europäischen Union ab 2009 in alle Neuwagen eingebaut werden.















Ihre Forschungsergebnisse stellen die Wissenschaftler unter Leitung des Saarbrücker Informatik-Professors Wolfgang Paul vom 9. bis 15. März 2006 auf der CeBIT in Hannover vor. In diesem Jahr ist das BMBF-Forschungsprojekt Verisoft am Stand des Bundesministeriums für Bildung und Forschung (Halle 9, Stand B40) vertreten.


Wenn bewiesen wird, dass Computersysteme ihre mathematisch exakten Vorgaben korrekt erfüllen, spricht man von formaler Verifikation. Die Methoden für die formale Verifikation von komplexen Computersystemen, die Soft- und Hardware umfassen, haben Wissenschaftler im Rahmen des Forschungsprojektes Verisoft entwickelt und an die Bedürfnisse der Industrie angepasst. Verisoft wird seit drei Jahren vom Bundesministerium für Bildung und Forschung (BMBF) gefördert und ist im vergangenen Jahr aufgrund seines Erfolgs mit weiteren 7,3 Mio. Euro ausgestattet worden.


Die Wissenschaftler des Verisoft-Projekts nehmen derzeit den automatischen Autonotruf eCall als Beispiel für ein komplexes verteiltes System unter die Lupe. Im Falle eines Unfalls alarmiert das eCall-System die Notrufkräfte und übermittelt ihnen die Fahrzeugposition sowie Informationen über die Schwere des Unfalls. Dieses verteilte System umfasst unter anderem ein Echtzeit-Betriebssystem sowie einen fehlertoleranten Kommunikationsbus. Neben der Fehlerfreiheit der einzelnen Komponenten muss auch deren korrektes Zusammenspiel über das Kommunikationssystem nachgewiesen werden.
"Bisher verwendet die Industrie viel Zeit darauf, Rechnersysteme zu testen, um dabei oft nur kleine Fehler zu entdecken. Sie sucht also sprichwörtlich die Nadel im Heuhaufen. Durch unser Verfahren können wir schon bei der Konstruktion jede auch noch so winzige Nadel im Heuhaufen finden", erläutert Professor Wolfgang Paul. Für die Industrie habe die Verifikation enorme Vorteile. Neue Systeme könnten schneller und günstiger entwickelt werden. Außerdem ersparten sich zum Beispiel die Autohersteller teure Rückrufaktionen wegen Entwurfsfehlern in der Fahrzeugelektronik. "Hier erhoffen wir uns einen Wettbewerbsvorteil für die bundesdeutsche Industrie, da die hiesige Forschung beim Thema Verifikation weltweit die Nase vorn hat", sagt der Saarbrücker Informatik-Professor.


Das Forschungsprojekt Verisoft wird von Professor Wolfgang Paul an der Universität des Saarlandes sowie Professor Manfred Broy an der TU München geleitet. Die akademischen Partner sind die Universität Koblenz, die Technischen Universitäten Darmstadt und München sowie das Deutsche Forschungszentrum für Künstliche Intelligenz (DFKI), das Max-Planck-Institut für Informatik in Saarbrücken und das Oldenburger Forschungs- und Entwicklungsinstitut für Informatikwerkzeuge und -systeme (OFFIS). Industrielle Partner sind die Infineon Technologies AG, die T-Systems International GmbH, die BMW Group AG und die mittelständischen Unternehmen OneSpin-Solutions GmBH und AbsInt GmbH.


Weitere Informationen unter: <www.verisoft.de.>


Der Leiter des BMBF-Forschungsprojekts Verisoft, Prof. Wolfgang Paul, wird über "Beweisbar korrekte Automobil-Elektronik - Korrektheitsbeweis für Prozessoren, Interfaces, Busse, Betriebssysteme, Compiler und Anwendungen" im future talk der CeBIT am Donnerstag, den 9. März um 15 Uhr referieren.
Weitere Informationen gibt es am Stand des Bundesministeriums für Bildung und Forschung (Halle 9, Stand B40) sowie am Stand der Universität des Saarlandes (Halle 9, Stand B43). Termine können unter Tel.: 0681/302-3585 vereinbart werden.


Pressefotos: Auf der Webseite <www.informatik-saarland.de> finden Sie ein Foto mit Prof. Wolfgang Paul zum Automotive-Teil von Verisoft.


Fragen beantworten Ihnen:
Projektleitung Verisoft
Tom In der Rieden
Tel.: 0681/302-3585
Email: idr@cs.uni-saarland.de
<www.verisoft.de>


Friederike Meyer zu Tittingdorf
Kompetenzzentrum Informatik an der Universität des Saarlandes
Tel.: 0681/302-58099
Email: presse@cs.uni-sb.de
<www.informatik-saarland.de>


Quelle: idw