Front-end Promela dans Spot

Auteurs

Guillaume Sadegh

Type

techreport

Année

2008

Numéro

0817

Projects

Spot

Mots-clés

Spot, model-checking, promela, virtual machine, promela front-end, Transition-based Generalized Büchi Automatamodeling language.

Résumé

Spot est une bibliothèque de model checking. Pour vérifier des modèles, Spot utilise un format 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ésenter, 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 plusieurs approches pour l'ajout d'un front-end Promela dans Spot, qui devront permettre une exploration à la volée du graphe d'états, afin d'éviter de conserver en mémoire tous les états.