Wir alle ärgern uns über Softwarefehler – von der Handy-App, die plötzlich abstürzt, bis zur Grafikkarte, die sich mit dem neuen Betriebssystem nicht verträgt. Beinahe haben wir uns schon daran gewöhnt, dass Computer manchmal unsicher, unvorhersehbar und fehleranfällig sind. Aber das müsste nicht so sein.

Prof. Laura Kovacs vom Institut für Logic and Computation der TU Wien entwickelt Methoden, mit denen unsere Software sicherer und verlässlicher werden soll. 2014 wurde sie mit einem ERC Starting Grant des European Research Council ausgezeichnet. Nun werden ihre Forschungserfolge mit einer weiteren ERC-Förderung belohnt: Mit Hilfe eines ERC Proof of Concept-Grants will Laura Kovacs ihre Ergebnisse nun in industrielle Anwendungen einbringen. Die Gründung eines eigenen Start-up-Unternehmens ist bereits geplant.

Mehr Software, mehr Fehler

Immer mehr Aspekte unseres Alltags werden von Software geregelt. Früher gingen wir zum Bankschalter, heute nutzen wir Online Banking. Früher war das Telefon mit dem Festnetz verbunden, heute brauchen wir Algorithmen, wie das Handy von Sendestation zu Sendestation weitergereicht werden kann. „Die Software wird immer umfangreicher und vielseitiger, aber ihre Verlässlichkeit steigt nicht“, sagt Laura Kovacs. „Wir arbeiten nach wie vor mit Software, die fehleranfällig ist und Sicherheitslücken hat.“

Je komplexer unsere Computerprogramme werden, umso schwieriger wird es für den Menschen, sie zu verstehen und nach Fehlern zu suchen. Man versucht daher heute, Computerprogramme zu entwickeln, die automatisch Fehler in anderen Computerprogrammen aufspüren können. Um dem Ziel der fehlerfreien, sicheren Software näher zu kommen, muss man auf die Methoden der formalen Logik zurückgreifen. Im Zuge ihres ERC-Projektes gelang es Laura Kovacs und ihrem Team, solche logischen Verfahren zu entwickeln und zu verbessern.

„Man kann Software formal in der Sprache der Mathematik beschreiben und dann beweisen, dass der Computercode bestimmte Eigenschaften hat“, erklärt Kovacs. „Dann muss man nicht mehr einfach darauf hoffen, dass das Programm auch in Zukunft die richtigen Ergebnisse liefern wird, man kann mit mathematischer Sicherheit beweisen, dass es in jeder beliebigen Situation die gewünschten Anforderungen erfüllt.“

Die neuen Methoden für die automatische Überprüfung von Software sind anderen, bisher verwendeten Methoden in wichtigen Aspekten überlegen – das zeigen Praxistests, bei denen die neuen Konzepte von Laura Kovacs‘ Arbeitsgruppe auf reale Computercodes aus der Industrie angewandt wurden. „Würde man Menschen ähnliche Beweise durchführen lassen, wäre das extrem aufwändig“, sagt Kovacs. „Aber mit unseren Logik-Methoden ist es bereits gelungen, das erwartete Verhalten der Software in 80 % der Fälle mathematisch zu garantieren.“

Der Schritt in die Praxis

Die theoretischen Erkenntnisse sollen nun industriell angewendet werden. Diesen Schritt unterstützt das European Research Council ERC nun mit einer weiteren Förderung – dem „Proof of Concept“-Grant. Laura Kovacs möchte nun nach Analyse des Marktes und noch besserer Anpassung der Konzepte an die Anforderungen der industriellen Praxis ein eigenes Start-up-Unternehmen gründen. „Das langfristige Ziel ist, Logik in der Softwareindustrie einzusetzen, um Softwarefehler zu finden und verlässlich zu korrigieren“, sagt Laura Kovacs.

Foto: Luiza Puiu