Verbesserung von Modellprüfung durch Programmanalyse

Softwaremodellprüfer stoßen häufig auf Grund ihres exorbitant großen Zustandsraums an ihre praktischen Grenzen. Typischerweise werden in Modellprüfern Programmvariablen auf Variablen mit einer bestimmten Bitbreite abgebildet. Dadurch wird der Zustandsraum endlich, aber praktisch zu groß. In diesem Projekt soll auf Modellebene durch Einblick in die innere Struktur der Zustände Optimierungen mit dem Ziel der Zustandsreduktion erarbeitet werden. Durch Anwendung klassischer aus dem Übersetzerbau bekannter Verfahren wie Elimination toter Variablen, Konstanten- und Kopienpropagation, Intervallanalyse und Slicing ist es gelungen, die Zustandsräume um Größenordnungen zu reduzieren. Anhand des Benchmarks aus dem Modellprüfer Moped, der an der Universität Stuttgart von der Arbeitsgruppe von Javier Esparza entwickelt wurde, konnte gezeigt werden, dass sich die Modellprüfungszeiten meist um den Faktor 10-100 reduziert. In einzelnen Fällen konnte nach der Optimierung komplett auf die Modellprüfung verzichtet werden, weil die zur Optimierung notwendigen Analysen die zu prüfende Eigenschaften bereits sicherstellt.