Verbesserung von Modellprüfung durch Programmanalyse
Projektleiter:
Projektbearbeiter:
Dipl.-Inform. Dirk Richter
Finanzierung:
Haushalt;
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.
Schlagworte
Modellprüfung, Programmanalyse, symbolische Kellersysteme
Publikationen
Die Daten werden geladen ...
Kontakt

Prof. Dr. Wolf Zimmermann
Martin-Luther-Universität Halle-Wittenberg
Naturwissenschaftliche Fakultät III
Von-Seckendorff-Platz 1
06120
Halle (Saale)
Tel.:+49 345 5524712
weitere Projekte
Die Daten werden geladen ...