Die Computertechnologie ist enorm fortgeschritten – kleine Software-Fehler und -Störungen scheinen aber nach wie vor unvermeidbar. Professor Laura Kovacs vom Institut für Logic and Computation an der TU Wien hat eine ergänzende Anwendung entwickelt, um Software sicherer und zuverlässiger zu machen.
Vom Telefonieren bis zum Online-Banking – unser Alltag ist zunehmend von Software bestimmt. Dabei wird unsere Erwartung an eine problemlose Funktion nicht immer erfüllt: Software-Fehler sind allgegenwärtig: Smartphone-Apps stürzen ab, Graphik-Karten sind nicht mit dem neuen Betriebs-System kompatibel, …
Zunehmende Komplexität
Laura Kovacs, Professor an der Fakultät für Informatik an der TU Wien führt Software-Fehler auf die zunehmende Komplexität von Programmen zurück. Dies erschwert deren Verständnis und die Suche nach Fehlern durch den Menschen. Die Computer-Industrie versucht das Problem mit Computer-Programmen zu lösen, die Fehler in Software erkennen. Theoretische Basis sind die Methoden der formalen Logik.
„Die Software wird immer umfangreicher und vielseitiger, aber ihre Verlässlichkeit steigt nicht“, sagt Kovacs. „Wir arbeiten nach wie vor mit Software, die fehleranfällig ist und Sicherheitslücken hat.“
Kovacs hat sich in ihrem aktuellen Projekt auf Safety & Critical Software spezialisiert, in dem es um Anwendungen für Online-Banking oder Flugtechnik geht. Gemeinsam mit ihrem Team ist es ihr gelungen, ein System zu entwickeln, das bestehende logische Verfahren verbessert. Als ergänzendes System ist dieses in bestehende Methoden zu integrieren. Die Innovation basiert auf einem automatisierten Algorithmus und einer Software, welche diesen ausführt.
„Es geht um die logische Beschreibung von Computer-Programmen und die Überprüfung der Logik “, erklärt Kovacs.
Mit dem Verfahren lässt sich das erwartete Verhalten der Software mit mathematischer Sicherheit prognostizieren.
Mit mathematischer Sicherheit
Das System wurde bereits ersten Praxistests in der Industrie unterzogen. Dabei konnte das Verhalten der Software in achtzig Prozent der Fälle mathematisch garantiert werden. Die ergänzende Methode kann in komplexen Datenstrukturen arbeiten und alle zu erkennenden Eigenschaften von Codes erfassen. Bestehende Methoden können nur in einfachen Datenstrukturen arbeiten.
Die Innovation wurde mit dem Proof of Concept Grant des ERC ausgezeichnet. Mit dieser Unterstützung will die Erfinderin jetzt ein Startup gründen. Die aktuelle Methode hat sich in kleinen akademischen Anwendungen bereits bewährt. Industrie-Anwendungen stellen eine größere Herausforderung dar. Kovacs: „Im akademischen Bereich arbeiten wir mit hundert Zeilen von Code. In Industrieprogrammen sind wir mit mindestens 100.000 Zeilen von Code konfrontiert.“
Kovacs war schon an der Entwicklung von Vampire beteiligt, einem vielfach ausgezeichneten Computer-Programm zur Überprüfung von Software.
Auch interessant:
Automatische Erkennung von Fake News mit Software von Fraunhofer
