KeY - Ein deduktives Software-Analyse-Werkzeug für die Forschungsgemeinschaft

• Antragsteller: Professor Dr. Bernhard Beckert; Dr. Richard Bubel; Professor Dr. Reiner Hähnle; Dr. Mattias Ulbrich
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Softwaretechnik und Programmiersprachen
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 443187992

Informatik spielt in der ablaufenden digitalen Revolution eine Schlüsselrolle und wird zur Basiswissenschaft. Grundlage des Paradigmenwechsels ist die Fähigkeit, hochzuverlässige Softwaresysteme zu verstehen, zu spezifizieren, zu implementieren und zu warten. Forscher (Informatiker zusammen mit Domänenexperten) müssen in die Lage versetzt werden, begründetes Vertrauen in ihre eigene Software zu erhalten. Ein Weg dahin ist die Anwendung formaler Analysewerkzeuge, welche rigorose, mathematisch begründete Garantien geben.Das KeY System ist ein kompetitives, statisches Analysewerkzeug für eine der populärsten Programmiersprachen: Java. KeY ist OpenSource und unter der GNU Public License veröffentlicht. KeY erlaubt es, Java Code formal zu spezifizieren und zu verifizieren. Es bietet die Möglichkeit, automatisch Testfälle zu erzeugen. Die Visualisierung von Abläufen als symbolischen Ausführungsbäume, hilft komplexe Programme zu verstehen und Fehler aufzuspüren.Hauptziel des Antrags ist die Robustheit und Nutzbarkeit von KeY so zu verbessern, dass andere Forscher aus der Informatik oder verwandter Bereiche in die Lage versetzt werden, KeY ohne Mitwirkung des KeY Teams erfolgreich für eigene Forschungsprojekte anzuwenden.KeY ist eine Umgebung für Experimente im Gebiet der formalen Methoden, wie auch eine Plattform zur Implementierung neuer Ansätze für die Sicherstellung und Analyse der Zuverlässigkeit von Forschungssoftware. Durch den Wechsel von physikalischen zu Softwarelösungen in allen Disziplinen, ist Software in der Pflicht, das Vertrauen in Forschungsresultate mit zu gewährleisten. In diesem Sinn wird Forschungssoftware vertrauenskritisch.Unsere Zielgruppe sind Forscher, die mit Methoden der Informatik an der Verbesserung von Softwaretechniken (Evolution, Entwicklung, Zuverlässigkeit, Sicherheit) arbeiten. Dies können Forscher aus Informatikfakultäten sein, aber auch, wie nun häufiger der Fall, Informatiker, die an Software in anderen Forschungsbereichen arbeiten.Die Projektarbeit ist in drei technische Bereiche gegliedert: (i) leichtere Nutzung durch verbesserte Zugänglichkeit, Eliminierung von Vorwissen, und einem geschlossenen Forschungszyklus Entwurf-Experiment-Analyse-Modifikation; (ii) verbesserte Robustheit: einfache Programme werden out-of-the-box analysiert, komplexe verursachen nie Abstürze und, falls nicht erfolgreich, gibt es hilfreiche Fehlermeldungen; (iii) Ermöglichung der Unterstützung anderer Programmiersprachen als Java. Die technischen Bereiche werden durch den Bereich Koordination komplementiert, mit nicht-technischen Paketen zu Infrastruktur, Dokumentation, Unterstützung der Nutzergemeinde.Das Projekt legt das Fundament, um eine aktive Forschergemeinde um KeY zu etablieren. Der Aufbau einer solchen ist essentiell, um nachhaltig (auch nach Projektende) sicherzustellen, dass KeY weiterentwickelt wird und um mit Neuerungen bei den unterstützten Zielsprachen Schritt zu halten.

• DFG-Verfahren: Sachbeihilfen