Front-end Promela dans Spot

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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.