Réduction d'ordre partiel 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.
- Auteurs
- Vincent Tourneur
- Type
- techreport
- Année
- 2017
- Numéro
- 1709
Résumé
Les outils de vérification formelle souffrent actuellement d'un problième de passage á l'échelleà cause de leur consommation de mémoire. La réduction d'ordre partiel est une des techniques permettant de la réduire notablement, en ne calculant que les données requises à la volée. Il en existe beaucoup d'algorithmes à l'état de l'art, et cette technique est utilisée dans plusieurs logiciels (comme SPIN ou LTSmin). Nous allons parler ici de l'implémentation de certains de ces algorithmes dans la bibliothèque Spot, puis de leur optimisation. Les résultats obtenus montrent une diminution notable de la consommation de mémoire, ce qui implique un gain pour toutes les étapes suivantes de la vérification.