Motivation
In heutigen Automobilen werden Fahreigenschaften, Komfort und Sicherheit maßgeblich durch eine Vielzahl von parallel arbeitenden Mini-Rechnern, sogenannten eingebetteten Systemen, bestimmt. Ein Hauptbestandteil dieser eingebetteten Systeme ist die Steuerungssoftware. Erst durch die Programmierung dieser Steuerungssoftware werden die Eigenschaften eines Automobils festgelegt. Allerdings kann z. B. eine fehlerhafte Programmierung oder nicht bedachte Wechselwirkungen zwischen den eingebetteten Systemen zu einem unerwünschten oder gar gefährlichen Betriebszustand (z.B. plötzlicher Stillstand des Fahrzeugs) führen. Aus diesem Grund muss die Korrektheit der hochkomplexen Software eines Automobils mit aufwendigen Verfahren gesichert werden. Die größte technische Herausforderung sind dabei die vielen, miteinander verbundenen Mini-Rechner, die in ihrer Gesamtheit das Rechnersystem eines Automobils ergeben. Es ist heutzutage sehr aufwendig bis unmöglich, formale Analysen (d.h. Verifikation) solcher Systeme in einem industriell relevanten Umfang (wie z. B. im Auto) mit einem hohen Genauigkeitsgrad durchzuführen.
Ziele und Vorgehen
Das Vorhaben HPSV hat zum Ziel, mit den Methoden des Hochleistungsrechnens neue Wege in der Softwareanalyse zu beschreiten und die Leistungsfähigkeit von Verfahren zur Verifikation komplexer Software auf ein bisher unerreichtes Niveau zu heben. Die Zusammenführung der beiden Gebiete Hochleistungsrechnen und Software-Verifikation stellt in diesem Umfang ein Novum dar. Im Projekt wird ein neuer, paralleler Verifikationsansatz für solche eingebetteten Systeme entwickelt. Die einzelnen Systeme werden im Hochleistungsrechner simuliert und alle möglichen Systemzustände ermittelt. Unerwünschte Zustände lassen sich so zusammen mit der Ursache ermitteln. Durch das Hochleistungsrechnen können so komplexerer Systeme simuliert und mit größerer Genauigkeit verifiziert werden.
Innovationen und Perspektiven
Die Konsortialpartner bringen unterschiedliche Kompetenzen in das Vorhaben ein. Das Zuse Institut Berlin verfügt zusammen mit den assoziierten Partnern Intel und Cray über die Kompetenz auf dem Gebiet des Hochleistungsrechnens. Die beiden Arbeitsgruppen der Christian-Albrechts-Universität zu Kiel arbeiten auf dem Gebiet der Software-Verifikation bzw. Modelltransformation. Die Unternehmen Elektronische Fahrwerksysteme GmbH (Gaimersheim), Model Engineering Solutions GmbH (Berlin) und Symtavision GmbH (Braunschweig) werden die neuen Verfikationstechniken sowohl in der modellbasierten Entwicklung als auch in der hardwarenahen Programmierung von eingebettetn Systemen im Automobilsektor anwenden. Die Ergebnisse dieses Projekts werden auch auf weitere Industriezweige übertragbar sein.