Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
P. Kaufmann, M. Kronegger, A. Pfandler, M. Seidl, M. Widl:
"Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines";
Vortrag: Workshop on Model Driven Engineering, Verification and Validation (MoDeVVa 2013),
Miami, USA;
01.10.2013; in: "Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation co-located with 16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013)",
CEUR Workshop Proceedings,
Vol-1069
(2013),
ISSN: 1613-0073;
S. 31
- 40.
Kurzfassung englisch:
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.
Schlagworte:
SAT, state machine, reachability analysis
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_220825.pdf
Zugeordnete Projekte:
Projektleitung Uwe Egly:
Quantified Boolean Formulas
Projektleitung Reinhard Pichler:
Effiziente, parametrisierte Algorithmen in Künstlicher Intelligenz und logischem Schließen
Projektleitung Martina Seidl:
FAME: Formalisierung und Handhabung von Evolution in modellbasierter Softwareentwicklung