| Software ohne Fehler ist ein Traum. In zwei Jahren wird er Realität. Das versprechen jedenfalls Informatiker der Saar-Uni. Sie testen im Projekt Verisoft das Zusammenspiel von Computer-Betriebssystemen und Anwendungsprogrammen. Zu ihren Forschungsschwerpunkten gehören Hard- und Software für die Autoindustrie.
Von SZ-Redakteur Peter Bylda
Saarbrücken. Die Affäre sorgt seit Monaten in Frankreich für Schlagzeilen: „La voiture folle“ („Das verrückte Auto“) ist die Geschichte eines Autofahrers, der am 3. Oktober 2004 auf der Autobahn A71 bei Clermont rund 150 Kilometer mit Tempo 200 durch die Landschaft raste – weil, wie er angab, der Tempomat seines Renault Vel Satis bei Vollgas blockiert war. Eine dreiviertel Stunde dauerte die Fahrt des Rennfahrers wider Willen, dann habe sich sein wild gewordenes Automobil ohne ersichtlichen Grund „beruhigt“, ohne dass sich ein Unfall ereignete, meldeten französische Zeitungen.
Software ohne Fehler
Der Fall beschäftigt jetzt die Gerichte. Acht Monate sitzen bereits zwei Gutachter über einer Expertise, in der es um die Frage geht, ob die Bordelektronik des „Voiture folle“ in den Vollgas-Wahn fiel oder ob ein Bedienungsfehler Auslöser der Autobahn-Raserei war.
Doch das, sagt der Saarbrücker Professor Dr. Wolfgang Paul, dauert nicht nur zu lang, sondern ist völlig unnötig. Statt umständlich nach möglichen Ursachen zu forschen, nachdem ein Problem in der Elektronik aufgetreten ist, wäre es besser, es grundsätzlich zu vermeiden. Das führt uns zur Frage: Ist garantiert fehlerfreie, sichere Computertechnik möglich? Kein Problem, erklärt der Informatiker der Saar-Uni und hat sich mit einer Mannschaft von 70 Wissenschaftlern aus ganz Deutschland daran gemacht, den Beweis dafür anzutreten.
Fürs Projekt „Verisoft“ hat das Bundesforschungsministerium in den vergangenen zwei Jahren bereits 3,4 Millionen Euro ausgegeben. Vor wenigen Tagen wurde die Förderung verdoppelt, um weitere zwei Jahre Forschung zu finanzieren. Verisoft ist nicht nur „weltweit einzigartig“, so sein Initiator nicht ganz frei von Eigenlob, sondern auch extrem ehrgeizig. Bis zum Ende der zweiten Phase will Pauls Mannschaft mit dem Chiphersteller Infineon die mathematische Korrektheit eines großen Industrie-Prozessors dieses Herstellers nachweisen. Zusätzlich soll am Labor-Prototyp eines künftigen Computer-Betriebssystems für Auto-Elektronik bewiesen werden, dass Software mit Null-Fehler-Garantie möglich ist.
Schon in diesem Jahr wollen die Informatiker ein Unternehmen gründen, das die Vermarktung dieses Wissens übernehmen soll. „Wir haben da sehr ernsthafte Anfragen aus der Industrie“, so Paul. Wenn für Hard- oder Software nachgewiesen wird, dass sie ihre Aufgaben präzise nach den Vorgaben erfüllt, sprechen Informatiker von „formaler Verfikation“. Der Beweis dafür führt unter anderem über Verfahren, die jeden Schritt, den ein Programm auf dem Weg vom Problem zur Lösung tut, in seine mathematischen Grundelemente zerlegen, um dann zu prüfen, ob sich jeweils das gewünschte Resultat ergibt. Andere Methoden fragen ab, ob einzelne Programmteile verbotene Zustände annehmen können, so wie eine Ampelanlage nicht gleichzeitig Autos und Fußgänger passieren lassen darf und ein Wasserhahn geschlossen sein muss, bevor die Wanne überläuft.
Auf Auto-Elektronik haben sich die Informatiker gestürzt, weil es hier nicht nur großes Interesse an sicherer Soft- und Hardware gibt, sondern noch größere Probleme. 1998 seien an 45 Prozent aller Auto-Pannen elektrische oder elektronische Probleme beteiligt gewesen, 2001 waren es bereits knapp 50 Prozent. Bei über drei Vierteln dieser Probleme spiele Software eine Rolle. Im Gegensatz zum PC-Nutzer kann der Autofahrer bei einer Panne aber nicht einfach den Reset-Knopf drücken und weiterfahren. Bei Rechner-Systemen im Auto kommt den Informatikern zupass, dass die Programme kompakt sind. Ihr sicherheitskritischer Bereich umfasst nur ein paar zehntausend Zeilen Code. Mit einem echten Computer-Betriebssystem, das tausend Mal umfangreicher ist, wären Verifizierungssysteme heute überfordert.
Es gibt außer der Kfz-Branche noch weitere Bereiche, in denen Programme mit Null-Fehler-Garantie Chancen haben. Die größten möglicherweise in Sachen Finanzen. In Deutschland kommt der Internet-Einkauf so recht nicht in Schwung, weil das Vertrauen in digitale Zahlungssysteme schwach ist. Das hat mit dem Misstrauen in die digitale Technik zu tun. So ganz sei dies auch nicht von der Hand zu weisen – Computer-Sicherheit ging bisher immer von der Sicherheit von Systemen aus, die nie verifiziert wurden, wirbt der Professor der Saar-Uni in eigener Sache. Oder drastischer: „Stellen Sie sich vor, Sie haben die schönsten Verschlüsselungsverfahren, aber ihr Betriebssystem ist gehackt.“
Wolfgang Paul ist überzeugt, dass das Etikett „Null-Fehler-Software: vom Betriebssystem bis zur Anwendung“ bald zu einem Verkaufsschlager erster Güte avancieren wird. „Und da haben wir die Nase vorn.“ Dank Verisoft besitze die Saar-Uni zwei bis drei Jahre Vorsprung vor der internationalen Konkurrenz. „Wir haben zwei bis drei Jahre Vorsprung vor der internationalen Konkurrenz.“
Auf die Schnelle
An mehr als der Hälfte der technischen Pannen unserer Autos ist die Elektronik schuld. Informatiker der Saar-Uni arbeiten im Projekt Verisoft an Techniken, die es erlauben, fehlerfreie Soft- und Hardware herzustellen. Die Forschung wird von der Bundesregierung mit insgesamt 6,8 Millionen Euro gefördert.
Mit freundlicher Genehmigung der Saarbrücker Zeitung |
