Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

GRK 1480:  PUMA Programm- und Modell-Analyse

Fachliche Zuordnung Informatik
Förderung Förderung von 2008 bis 2017
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 47140942
 
Erstellungsjahr 2018

Zusammenfassung der Projektergebnisse

Die Hauptaufgabe der Programm- und Modell-Analyse ist das Aufdecken von Fehlern bzw. der Nachweis, dass ein Programm oder Modell korrekt ist, d.h. sich gemäß seiner Spezifikation verhält. Eine solche Spezifikation kann etwa verlangen, dass Verklemmungen von Threads oder Laufzeitfehler wie illegale Speicherzugriffe nicht vorkommen. Sie könnte aber auch genaue Vorgaben über den Ressourcenverbrauch oder das Ein/Ausgabe-Verhalten machen. Ausgangspunkt der Forschung im Graduiertenkolleg PUMA sind die vier gängigen Ansätze zur Lösung solcher Probleme: Programm-Verifikation durch Theorembeweisen, Model Checking, Statische Analyse durch Abstrakte Interpretation und Typsysteme. Die tragende Hypothese des Graduiertenkollegs war, dass diese Ansätze, obwohl sie traditionellerweise von unterschiedlichen Communities verfolgt werden, nur scheinbar unvereinbar sind, dass vielmehr die Interaktion, der Austausch zwischen diesen Herangehensweisen zu neuen, möglicherweise besseren Verfahren führen würde. Diese Annahme hat sich im Laufe der ersten drei Jahre und nicht zuletzt durch die Beiträge des Graduiertenkollegs bestätigt: seitdem entwickelt sich die Forschung weltweit in diese Richtung. Das Zusammenwachsen von logischen Entscheidungsprozeduren, Model Checking und abstrakter Interpretation hat sich mittlerweile als eine Einheit etabliert. Der bei Microsoft Research entwickelte SMT-Solver Z3 wird mittlerweile in vielen Werkzeugen für Model Checking, Testing, und Programmanalyse als Back-End eingesetzt. Die Wiederbelebung der Hoarelogik durch Automatisierung und begleitende abstrakte Interpretation hat sich fortgesetzt. Das Ziel des Graduiertenkollegs der ersten Periode, Möglichkeiten zur Kombination der vier Ansätze der Programm- und Modellanalyse auszuloten, wurde deshalb für die zweite Förderperiode verfeinert. Bei einer Logik-basierten Formulierung der Programm- und Modellanalyse ist eine Verbesserung der Entscheidungsprozeduren und Löser von essentieller Bedeutung. Die Constraint-Lösungsalgorithmen aus der ersten Periode wurden deshalb in der zweiten Periode aufgegriffen und weiter verallgemeinert. Neue besser korrekt zu beweisende Verfahren wurden für MSO entwickelt. Ganz neu traten Löser für gewöhnliche Differentialgleichungen in den Fokus des Interesses, da mit ihnen verifizierte Erreichbarkeitsanalysen für cyber-physikalische Systeme konstruiert werden können. Ebenfalls aufgegriffen wurde das Konzept generischer lokaler Fixpunktalgorithmen, die um die Möglichkeit, mit Widening und Narrowing umzugehen, erweitert wurden. Solche Algorithmen bilden das Herz praktischer Programmanalysesysteme. Entscheidende Fortschritte gab es auch in der zweiten Förderperiode bei probabilistischem Model Checking, für das in der ersten Periode verifizierte Implementierungen geliefert wurden. Hier wurden ganz neue und besser skalierende Verfahren gefunden. Ebenfalls in der zweiten Periode weiter geführt wurden die Untersuchung der neuen typbasiertem Techniken zur Analyse des Speicherplatzverbrauchs. Konnten in der ersten Periode Methoden für funktionale, objektorientierte und reaktive Programmiersprachen entwickelt werden, so blieb doch die Lösbarkeit der bei der Analyse objektorienter Programme auftretenden Constraint Systeme offen. Hier konnte erst in der zweiten Förderperiode nachgewiesen werden, dass diese tatsächlich entscheidbar sind. Ein besonderes Highlight in der ersten Periode war die Realisierung eines Werkzeugs zur automatischen Lösung von Syntheseproblemen für Kontrolleinheiten von industriellen Automatisierungsprozessen. In der zweiten Periode dienten autonome Systeme als ein praktisch relevantes Anwendungsszenario. Dieses erwies sich als sehr fruchtbar, da es das Erfordernis einer Formalisierung von Verkehrsregeln mit sich brachte und zu einer Untersuchung von beweisbar sicherem Fahrzeugverhalten anregte.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2025 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung