Berechnung von Gegenbeispielen für stochastische Systeme unter Verwendung von Bounded Model Checking

• Antragstellerin: Professorin Dr. Erika Ábrahám
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2010 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 183345248

Für die Korrektur fehlerhafter Systeme ist es von entscheidender Bedeutung, Gegenbeispiele zur Hand zu haben. Gegenbeispiele sind Abläufe eines Systems, die zu fehlerhaftem Verhalten führen. Bisherige Arbeiten über die Analyse stochastischer Systeme konzentrierten sich auf die Berechnung der Wahrscheinlichkeit, mit der Abläufe eines stochastischen Systems eine vorgegebene Eigenschaft erfüllen. Falls diese Wahrscheinlichkeit außerhalb der zulässigen Grenzen liegt, liefern die bisher bekannten Model-Checking-Algorithmen nur die berechneten Wahrscheinlichkeitswerte, aber kein Gegenbeispiel. Erste Arbeiten in Richtung Gegenbeispielgenerierung für stochastische Systeme betrachten Markow-Ketten mit diskreter Zeit, eine relativ einfache Klasse von stochastischen Systemen. Ziel dieses Projektes ist, zum einen die vorhandenen Technologien zur Gegenbeispielgenerierung zu verbessern und zum anderen Algorithmen für ausdrucksstärkere Logiken und mächtigere Systeme zu entwickeln und zu implementieren. Wir wollen ihre praktische Anwendbarkeit anhand einer Reihe von Benchmarks nachweisen.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Personen: Professor Dr. Bernd Becker; Professor Dr. Joost-Pieter Katoen