Petra Kaufmann, Andreas Pfandler, Martin Kronegger, Martina Seidl, Magdalena Widl,
""Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines"
: Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation, Serie CEUR Workshop Proceedings, Vol. 1069, Seite(n) 31-40, 1-2013, ISBN: 1613-0073
"Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines
Sprache des Titels:
Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation
We present a novel propositional encoding for the reachability problem of communicating state machines. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios.
By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in
propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.