Réduction d'ordre partiel dans SPOT

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.