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

(S)SBMC

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Bettina Braitling, Dipl.-Inf. Entwickler / Kontakt
Ralf Wimmer, Dr. Entwickler / Kontakt


Beschreibung

(S)SBMC berechnet Gegenbeispiele für probabilistische Systeme in Form von Markov-Ketten mit diskreter Zeit (DTMCs) oder Markov Reward-Modellen (MRMs) mit diskreter Zeit. Es wird eine Menge von Pfaden berechnet, die eine bestimmte Eigenschaft erfüllen. Die Gesamt-Wahrscheinlichkeit dieser Menge liegt über einer gegebenen Wahrscheinlichkeitsschranke. Die Berechnung basiert auf Bounded Model Checking, wobei entweder der SAT-Solver MiniSat (bei SBMC) oder der SMT-Solver Yices (bei SSBMC) verwendet wird. Es gibt einige zusätzliche Funktionen:
- Schleifenerkennung beschleunigt die Berechnung
- Bisimulationsminimierung verkleinert das System
- Pfadkonvertierung wandelt minimierte Pfade um in Original-Pfade.
Die SMT-basierte Variante SSBMC ermöglicht es, Pfade mit höherer Wahrscheinlichkeit zuerst zu finden, wodurch ein kleineres Gegenbeispiel berechnet werden kann als mit SAT. SSBMC ist außerdem in der Lage, Gegenbeispiele für MRMs zu berechnen. In diesem Fall kann der Suchraum auf ein gegebenes Reward-Intervall beschränkt werden, so dass nur noch Pfade mit einem Reward innerhalb dieses Intervalls betrachtet werden.



Benchmarks

- Contract Signing Protocol (*)(**)
- Crowds Protocol (*)(**)
- Synchronous Leader Election Protocol (*)(**)
- Self-stabilizing Minimal Spanning-Tree (**)

(*) http://www.prismmodelchecker.org/casestudies/index.php
(**) http://www.avacs.org/benchmarks/



Publikationen
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham
SMT-based Counterexample Generation for Markov Chains
GI/ITG/GMM Workshop: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011
Ralf Wimmer, Bettina Braitling, Bernd Becker
Counterexample Generation for Discrete-time Markov Chains using Bounded Model Checking
Int'l Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI), 2009
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham
Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking
IFIP Int'l Conf. on Formal Methods for Open Object-based Distributed Systems / IFIP Int'l Conf. on Formal Techniques for Networked and Distributed Systems, 2011