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
- [KP07]
-
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
[pdf | slides]
- [Kem06]
-
Stephanie Kemper.
SAT-based Verification for Abstraction Refinement.
University of Oldenburg, Jan. 2006
[pdf]
The slides are Copyright © 2006 Stephanie Kemper.
|
