A Promela front-end for Spot
Guillaume Sadegh · 2008
SPOT is a C++ library for model-checking. For verification, SPOT uses an input-format that describes a Transition-based Generalized Büchi Automata (TGBA). However, this format does not seem accessible for users with its poor abstraction and with the size of automata which often have millions of states. PROMELA (Process Meta-Language) is the verification modeling language used by the SPIN model checker. It lets users describe a parallel system for verification in a high level programming language. We present a way to add a PROMELA front-end in SPOT, which will allow to explore the state-graph on-the-fly and thus avoid to store all the states of our automata. SPOT est une bibliothèque de model checking écrite en C++. Pour vérifier des modèles, SPOT utilise un for-mat d’entrée représentant des automates de Büchi généralisés basés sur les transitions (TGBA). Ce format est peu pratique pour des utilisateurs, par son manque d’abstraction et par la taille des automates à représen-ter, souvent composés de millions d’états. PROMELA (Process Meta-Language) est un langage de spécification de systèmes asynchrones, utilisé par le model checker SPIN. Il permet de représenter des systèmes concurrents dans un langage impératif de haut niveau. Nous allons présenter une approche pour l’ajout d’un front-end PROMELA dans SPOT, qui devra per-mettre une exploration à la volée du graphe d’états, afin d’éviter de conserver en mémoire tous les états.