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
