Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

CEBug

| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Bernd Becker, Prof. Dr. Kontakt
Ralf Wimmer, Dr. Kontakt
Bettina Braitling, Dipl.-Inf. wissenschaftlicher Mitarbeiter
Kooperationspartner

RWTH Aachen
Erika Ábrahám, Prof. Dr. Kontakt
Joost-Pieter Katoen, Prof. Dr. Kontakt
Nils Jansen, Dipl.-Inf. wissenschaftlicher Mitarbeiter


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.