A Promela front-end for Spot
From LRDE
- Authors
- Guillaume Sadegh
- Type
- techreport
- Year
- 2008
- Number
- 0817
- Projects
- Spot
- Keywords
- Spot, model-checking, promela, virtual machine, promela front-end, Transition-based Generalized Büchi Automatamodeling language.
Abstract
Spot is a C++ library for model checking. For verification, Spot uses an input-format which describes a Transition-based Generalized Büchi Automata (TGBA). However, this format doesn't seem accessible for users with its poor abstraction and the need for often representing automaton with millions of states. Promela (Process Meta-Language) is a verification modeling language used by the Spin model checker. It lets users to describe a parallel system for verification in a high level programming language. We will present different ways to add a Promela front-end in Spot, which will allow to explore the state-graph on-the-fly, in order to avoid storing all the states.