[Zurück zum
Forschungsbericht]

CEBug

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.

Weitere Informationen: http://ira.informatik.uni-freiburg.de/src/projects_view.php?projectID=57
Ansprechpartner: Wimmer R
Projektlaufzeit:
Projektbeginn: 2011
Projektende: (unbegrenzt)
Projektleitung:
Becker B

Albert-Ludwigs-Universität Freiburg


Mitarbeiter:
  • Wimmer
  • Braitling
Projektbezogene Publikationen:

  • Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster: Symbolic Counterexample Generation for Large Discrete-Time Markov Chains Sci Comput Program, 2014; 91 (A): 90-114. : http://dx.doi.org/10.1016/j.scico.2014.02.001
  • Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker: Minimal Counterexamples for Linear-Time Probabilistic Verification Theor Comput Sci, 2014. : https://dx.doi.org/10.1016/j.tcs.2014.06.020 (in Druck)
  • Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám: Stochastic Bounded Model Checking: Bounded Rewards and Compositionality GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2013: 243-254.
  • Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker: High-Level Counterexamples for Probabilistic Automata 2013; arxiv:1305.5055. (download: http://arxiv.org/abs/1305.5055)
  • Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker: High-Level Counterexamples for Probabilistic Automata 2013; 8054: 18-33, Springer-Verlag (Hrsg). : http://dx.doi.org/10.1007/978-3-642-40196-1_4
  • Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker: The COMICS Tool - Computing Minimal Counterexamples for DTMCs 2012; arxiv:1206.0603. (download: http://arxiv.org/abs/1206.0603)
  • Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen: Minimal Critical Subsystems for Discrete-Time Markov Models Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2012; 7214: 299-314, Springer-Verlag (Hrsg). : http://dx.doi.org/10.1007/978-3-642-28756-5_21

Aktueller Forschungsbericht