Der Autopilot in einem Flugzeug muss fehlerfrei funktionieren. Ebenso die Software von Steuerungs- und \u00dcberwachungssystemen im Bahnverkehr. Auch bei selbstfahrenden Autos h\u00e4ngen Menschenleben davon ab, dass sich die Technik jederzeit korrekt verh\u00e4lt. InformatikerInnen der Uni Siegen arbeiten daran, die Software f\u00fcr solche Anwendungen zu verbessern. Im Projekt \u201eComputing with Infinite Data\u201c (CID) kooperieren die ForscherInnen dazu mit \u00fcber 20 Partneruniversit\u00e4ten und \u2013Instituten in aller Welt. Die EU f\u00f6rdert das Projekt im Rahmen des Programms \u201eHorizon 2020\u201c mit knapp einer Millionen Euro.<\/p>\n
\u201eWir haben bisher keine M\u00f6glichkeit, die mathematische Theorie eins-zu-eins in der Programmiersprache abzubilden\u201c, erkl\u00e4rt Prof. Dr. Dieter Spreen von der Uni Siegen, der das Projekt gemeinsam mit seinem Kollegen Prof. Dr. Markus Lohrey leitet. Ein Problem stellen den Experten zufolge die vielen noch aus der Schule bekannten Dezimalbr\u00fcche dar: Sie k\u00f6nnen in den Programmen nicht komplett abgebildet werden, was Rundungsfehler zur Folge hat. \u201eEin Ziel unserer Forschung ist es, dieses Missverh\u00e4ltnis zwischen mathematischer Theorie und dem, was im Rechner passiert, aufzuheben und so Ungenauigkeiten in den Programmen zu beheben\u201c, sagt Spreen.<\/p>\n
Gleichzeitig m\u00f6chten die ForscherInnen im Rahmen des CID-Projektes eine M\u00f6glichkeit entwickeln, die korrekte Funktionsweise von Ingenieur-Anwendungen formal zu beweisen. \u201eBisher wird etwa die Software f\u00fcr Flugzeug-Autopiloten umfangreich getestet, bevor sie zum Einsatz kommt. Sollten dennoch Sicherheitsl\u00fccken auftreten, m\u00fcssen sie nachtr\u00e4glich geschlossen werden\u201c, erkl\u00e4rt Professor Spreen. Unter Verwendung unendlich-pr\u00e4ziser Daten soll es in Zukunft m\u00f6glich sein, formal zu beweisen, dass Programme entsprechend der jeweiligen Vorgaben funktionieren. Tests w\u00e4ren damit \u00fcberfl\u00fcssig, Sicherheitsl\u00fccken k\u00f6nnten vorab ausgeschlossen werden. \u201eEin solches Verfahren w\u00e4re zuverl\u00e4ssiger, als das bisherige\u201c, ist Spreen \u00fcberzeugt. \u201eWir h\u00e4tten dann zertifizierte Programme, die mit hundertprozentiger Sicherheit korrekt arbeiten.\u201c<\/p>\n
In einem weiteren Teilbereich des Projektes besch\u00e4ftigen sich die WissenschaftlerInnen mit verschiedenen Rechenverfahren in Ingenieuranwendungen. \u201eWir m\u00f6chten die Verfahren hinsichtlich ihres Rechenaufwandes vergleichen und eine Theorie dazu entwickeln\u201c, erl\u00e4utert Spreen. F\u00fcr manche Problemstellungen gebe es aufgrund ihrer Komplexit\u00e4t auch schlicht keine einfachen Verfahren. Auch diese Erkenntnis sei f\u00fcr Anwender und Forscher wertvoll, da sie in solchen F\u00e4llen nicht mehr unn\u00f6tig und zeitaufw\u00e4ndig nach Alternativen suchen m\u00fcssten.<\/p>\n
Das Verbund-Projekt wird von der Universit\u00e4t Siegen koordiniert und startet am 1. April 2017. In Deutschland sind neben der Uni Siegen noch die Universit\u00e4t Trier, die FH Dortmund und die LMU M\u00fcnchen beteiligt, hinzu kommen Partnerschaften mit verschiedenen europ\u00e4ischen Universit\u00e4ten, aber auch mit Institutionen zum Beispiel in Japan, Korea, S\u00fcdafrika oder Chile. \u201eComputing with Infinite Data\u201c sei das teilnehmerst\u00e4rkste Projekt im Rahmen der Ausschreibung, sagt Prof. Spreen. Mit den F\u00f6rdermitteln sollen vor allem gegenseitige Besuche der WissenschaftlerInnen finanziert werden: Sie wollen die mehrmonatigen Forschungsaufenthalte dazu nutzen, Wissen auszutauschen und voneinander zu lernen. Einmal pro Jahr ist dar\u00fcber hinaus ein offener Workshop geplant. Die Laufzeit des Projektes betr\u00e4gt insgesamt vier Jahre.<\/p>\n