Counterexample generation for stochastic systems using Bounded Model Checking

• Applicant: Professorin Dr. Erika Ábrahám
• Subject Area: Software Engineering and Programming Languages
• Term: from 2010 to 2015
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants
• Participating Persons: Professor Dr. Bernd Becker; Professor Dr. Joost-Pieter Katoen