Title :
SPOT: an extensible model checking library using transition-based generalized Büchi automata
Author :
Duret-Lutz, Alexandre ; Poitrenaud, Denis
Author_Institution :
Lab. d´´Informatique de Paris 6, Univ. Pierre et Marie Curie, Paris, France
Abstract :
SPOT (SPOT produces our traces), is a C++ library offering model checking bricks that can be combined and interfaced with third party tools to build a model checker. It relies on transition-based generalized Büchi automata (TGBA) and does not need to degeneralize these automata to check their emptiness. We motivate the choice of TGBA by illustrating a very simple (yet efficient) translation of LTL (linear temporal logic) into TGBA. We then show how it supports on-the-fly computations, and how it can be extended or integrated in other tools.
Keywords :
C language; automata theory; object-oriented methods; software libraries; temporal logic; C++ library; extensible model checking library; linear temporal logic; model checker; object-oriented library; transition-based generalized Buchi automata; Automata; Computational modeling; Computer interfaces; Impedance; Libraries; Logic; Object oriented modeling; Pipelines; State-space methods; Telecommunication computing;
Conference_Titel :
Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004. (MASCOTS 2004). Proceedings. The IEEE Computer Society's 12th Annual International Symposium on
Print_ISBN :
0-7695-2251-3
DOI :
10.1109/MASCOT.2004.1348184
