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

Projekte

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.

Laufzeit

Von 01.01.2011 (unbegrenzt)

Projektleitung

Becker B

Ansprechpartner/in

Wimmer R

Publikationen


Jahre: 2015 | 2014 | 2013 | 2012 | 2011

    2015

    Icon: top nach oben zur Jahresübersicht
    • Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
      Counterexamples for Expected Rewards
      2015 Proceedings of the 20th International Symposium on Formal Methods (FM), Springer, Band: 9109, Seiten: 435 - 452
    • Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
      High-level Counterexamples for Probabilistic Automata
      2015 Log Meth Comput Sci (Logical Methods In Computer Science), Band: 11, Nummer: 1:15, Seiten: 1 - 23

    2014

    Icon: top nach oben zur Jahresübersicht
    • Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer
      Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
      In: International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), Advanced Lectures
      2014, Springer-Verlag, Seiten: 65 - 121,
    • Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
      Fast Debugging of PRISM Models
      2014 Int'l Symp. on Automated Technology for Verfication and Analysis, Springer-Verlag
    • Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
      Minimal Counterexamples for Linear-Time Probabilistic Verification
      2014 Theor Comput Sci
    • 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
      2014 Sci Comput Program, Band: 91, Nummer: A, Seiten: 90 - 114

    2013

    Icon: top nach oben zur Jahresübersicht
    • Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
      High-Level Counterexamples for Probabilistic Automata
      2013 Springer-Verlag, Band: 8054, Seiten: 18 - 33
    • Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
      High-Level Counterexamples for Probabilistic Automata
      , Band: arxiv:1305.5055, 2013
    • Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám
      Stochastic Bounded Model Checking: Bounded Rewards and Compositionality
      2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 243 - 254

    2012

    Icon: top nach oben zur Jahresübersicht
    • Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
      Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
      AVACS Technical Report, Nummer: 88, 2012
    • Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
      Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties
      2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Verlag Dr. Kovac, Seiten: 169 - 180
    • Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
      Minimal Critical Subsystems for Discrete-Time Markov Models
      2012 Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer-Verlag, Band: 7214, Seiten: 299 - 314
    • Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker
      Symbolic Counterexample Generation for Discrete-time Markov Chains
      2012 Int'l Symp. on Formal Aspects of Component Software, Springer-Verlag, Band: 7684, Seiten: 134 - 151
    • Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
      The COMICS Tool - Computing Minimal Counterexamples for DTMCs
      2012 Automated Technology for Verification and Analysis, Springer-Verlag, Band: 7561, Seiten: 349 - 353
    • 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
      , Band: arxiv:1206.0603, 2012

    2011

    Icon: top nach oben zur Jahresübersicht
    • Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
      Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking
      2011 IFIP Int'l Conf. on Formal Methods for Open Object-based Distributed Systems, Springer-Verlag, Band: 6722, Seiten: 75 - 89
    • Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
      Hierarchical Counterexamples for Discrete-Time Markov Chains
      2011 Int'l Symp. on Automated Technology for Verification and Analysis, Springer-Verlag, Band: 6996, Seiten: 443 - 452
    • Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
      Hierarchical Counterexamples for Discrete-Time Markov Chains
      , Band: AIB-2011-11, 2011
    • Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
      SMT-based Counterexample Generation for Markov Chains
      2011 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Offis Oldenburg, Band: 14, Seiten: 19 - 28