Overview
SAAtRe is an abstraction refinement model checker for timed automata based on extended SAT-solving techniques. In joint work, SAAtRe has been implemented by Stephanie Kemper at the University of Oldenburg and the Centrum voor Wiskunde en Informatica (CWI). In addition to transition constraint system input, SAAtRe has an input format for timed automata like the UPPAAL XML format.
 |
 |
Abstract
In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. With a faithful embedding of bounded model checking for systems of timed automata into propositional logic and linear arithmetic, we achieve both, quick abstraction techniques and a linear-size representation of parallel composition. In this logical setting, we introduce an abstraction that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexample-guided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logic-based abstraction refinement.
Keywords: abstraction refinement, model checking, real-time systems, SAT, Craig interpolation
-
Stephanie Kemper and André Platzer.
SAT-based abstraction refinement for real-time systems.
In Frank S. de Boer and Vladimir Mencl, editors, Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, Electr. Notes Theor. Comput. Sci., 182:107-122, 2007
[bib | ✂ | pdf | doi | slides | tool | abstract]
-
Stephanie Kemper.
SAT-based Verification for Abstraction Refinement.
University of Oldenburg, Jan. 2006
Also see publications on model checking.