Model-Checking von Navigationslogiken (MoNaLog)

• Antragsteller: Professor Dr. Markus Müller-Olm
• Fachliche Zuordnung: Theoretische Informatik ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2020 bis 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 436811065

Software ist oft kritischer Bestandteil von Systemen, deren Ausfall ernsthafte Konsequenzen nach sich ziehen kann, wie massive finanzielle Schäden oder gar Gefahren für Leib und Leben. Verlässlichkeit von Software ist deshalb ein Kernproblem der Informatik. Klassische Validierungsverfahren wie Testen oder Simulation sind aus prinzipiellen Gründen in aller Regel nicht in der Lage, starke Korrektheitsgarantien zu geben, da sie nur eine Auswahl der möglichen Programmausführungen betrachten. Dieses Problem wird durch die zunehmende Präsenz von Nebenläufigkeit (Parallelität) in modernen Systemen, die in der Regel mit nicht-deterministischem Verhalten einhergeht, weiter verschärft. Deshalb wurden formale Methoden der Programmverifikation entwickelt, die auf Techniken der Mathematik und der mathematischen Logik basieren und die prinzipiell in der Lage sind, starke Garantien zu liefern. Die klassische Programmverifikation z. B. à la Floyd-Hoare ist allerdings nur teilweise automatisierbar. Deshalb ist ihre Integration in traditionelle Softwareentwicklungsmethoden schwierig. Aus diesem Grund wurden seit den 1980er Jahren vollautomatische Verifikationsverfahren entwickelt, insbesondere das sogenannte Model-Checking, bei dem algorithmisch entschieden wird, ob eine Programmabstraktion eine Spezifikation erfüllt, die durch eine temporallogische Formel gegeben ist. Ziel des beantragten Projekts ist die Entwicklung und Untersuchung neuartiger temporaler Logiken, die es erlauben, bei der Formulierung von Eigenschaften zusätzlich zur üblichen Navigation über die temporale, rein sequentielle Abfolge von Aktionen auch charakteristische Aspekte der Art und Weise, wie das Systemverhalten strukturiert beschrieben ist, zu reflektieren. Im Fokus steht dabei die Navigation im Zusammenhang mit komplexen Kontrollstrukturen, insbesondere solchen zur Beschreibung von Rekursion und Multi-Threading. Im Rahmen des Projekts sollen Logiken entwickelt werden, die existierende temporale Logiken um entsprechende Konzepte erweitern und für die das Model-Checking-Problem effektiv bleibt. Für die neuen Logiken und die dazugehörigen Klassen von Systemmodellen sollen die Komplexität des Model-Checking-Problems untersucht und Model-Checking-Algorithmen entwickelt werden. Die Model-Checking-Algorithmen sollen prototypisch implementiert und an charakteristischen Benchmarks evaluiert werden. Darüber hinaus sollen auch weitergehende Aspekte wie die Entscheidbarkeit des Erfüllbarkeitsproblems untersucht werden.

• DFG-Verfahren: Sachbeihilfen