Wissenschaftler der Universität Paderborn wollen Softwareverifikation verbessern
Läuft meine Software korrekt, sicher und zuverlässig? Seit Jahrzehnten nutzen Softwareentwickler verschiedene Ansätze der sogenannten Softwareverifikation, um die Eigenschaften ihrer Programme zu prüfen. So lässt sich sicherstellen, dass Unternehmen, Behörden und private Nutzer qualitativ hochwertige Software erhalten und Softwarefehler, die fatale Folgen haben können, möglichst ausbleiben. In einem neuen Forschungsprojekt wollen Prof. Dr. Heike Wehrheim und ihr Team vom Fachgebiet „Spezifikation und Modellierung von Softwaresystemen“ des Instituts für Informatik der Universität Paderborn die Präzision und Performance bereits existierender Ansätze der Softwareverifikation verbessern. Das dreijährige Projekt „Cooperative Software Verification“ wird von der Deutschen Forschungsgemeinschaft (DFG) gefördert und zusammen mit Prof. Dr. Dirk Beyer und seinen Mitarbeitern vom „Software and Computational Systems Lab“ der Ludwig-Maximilians-Universität München durchgeführt. Die Universität Paderborn erhält 253.800 Euro Fördermittel.
Bereits 1949 entwickelte der Brite Alan Turing, einer der einflussreichsten Theoretiker der frühen Informatik, einen ersten Ansatz der Softwareverifikation, mit dem sich prüfen lässt, ob Computerprogramme korrekt arbeiten. „In den letzten Jahren wurden im Bereich der Softwareverifikation enorme Fortschritte erzielt“, erklärt Heike Wehrheim. „Entwicklern stehen heute viele Ansätze der Softwareverifikation zur Verfügung, die von dynamischer bis zu statischer Analyse reichen und besondere Stärken, aber auch Schwächen haben. Hier setzt unser Forschungsprojekt an, indem es hilft, die bestehenden Ansätze zu verbessern. Das ist vor allem in sicherheitskritischen Bereichen wie eingebetteten Systemen und Systemsoftware notwendig, um die Sicherheit von Software zu garantieren“, führt die Informatikerin aus.
Die Wissenschaftler aus Paderborn und München wollen die Präzision und Performance bereits existierender Ansätze von Softwareverifikation verbessern, indem sie verschiedene Werkzeuge und Techniken verbinden, die bei der Softwareverifikation genutzt werden. „In unserem Forschungsprojekt wollen wir eine praktische Methodik der kooperativen Softwareverifikation und die dahinterliegende Theorie der Kooperation entwickeln“, erläutert Wehrheim. Der Ansatz der Wissenschaftlerin und ihrer Kollegen: Bei der Prüfung der Eigenschaften von Computerprogrammen werden Verifikationsaufgaben auf Werkzeuge aufgeteilt, sodass jedes Werkzeug die Aufgaben erledigt, für die es am besten geeignet ist. „In unserem Projekt wollen wir Methoden entwickeln, die es den Verifikationswerkzeugen ermöglichen, Informationen auszutauschen und diese korrekt zu nutzen. Außerdem sollen Verfahren entwickelt werden, die zeigen, wann und wie die Verifikationswerkzeuge am besten kooperieren können“, so Wehrheim. Die angestrebte kooperative Softwareverifikation soll außerdem das Vertrauen in die Gültigkeit von Verifikationsergebnissen erhöhen – etwa, indem ein Werkzeug das Ergebnis eines anderen Werkzeugs überprüft.
Erste Ergebnisse des Forschungsprojekts werden Ende 2020 erwartet.
Weitere Informationen: https://cs.uni-paderborn.de/sms/research/cooperative-software-verification
Simon Ratmann, Stabsstelle Presse und Kommunikation
Titelfoto: Pixabay / Free-Photos / CC0 1.0, https://creativecommons.org/publicdomain/zero/1.0/deed.de
