A Promela front-end for Spot

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.