CEBug

| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung |

Um Fehler in Systemen beheben zu können, ist es essentiell, Gegenbeispiele zur Hand zu haben. Gegenbeispiele sind dabei Systemabläufe die zu einem fehlerhaften Verhalten des Systems führen. Die bisherige Forschung zu stochastischen Systemen konzentrierte sich auf die Berechnung von Wahrscheinlichkeiten, mit denen die Abläufe eines stochastischen Systems eine vorgegebene Eigenschaft erfüllen. Wenn diese Wahrscheinlichkeiten nicht innerhalb der zulässigen Schranken liegen, liefern die verfügbaren Algorithmen zur Modellprüfung zwar die genauen Wahrscheinlichkeitswerte, jedoch keine Gegenbeispiele.

Die ersten Schritte zur Berechnung von Gegenbespielen betrachten Markov-Ketten mit diskreter Zeit, eine relativ einfache Klasse von stochastischen Systemen. Das Ziel dieses Projekts ist, auf der einen Seite die verfügbaren Techniken zur Berechnung von Gegenbeispielen zu verbessern und auf der anderen Seite Verfahren zu entwickeln un dzu implementieren, die mit ausdrucksstärkeren Eigenschaften und reichhaltigeren Systemen zurecht kommen. Die praktische Anwendbarkeit unserer Algorithmen werden wir anhand einer Menge von Benchmarks nachweisen.

Dieses Projekt wird durch die Deutsche Forschungsgemeinschaft (DFG) gefördert.