Mesures sur la réduction d'ordre partiel dans Spot

Auteurs

Vincent Tourneur

Type

techreport

Année

2019

Numéro

1901

Résumé

Ce rapport résume trois méthodes implémentées dans l'outil de vérification de modèles Spot. La première vise à améliorer la conversion de modèle de programme en structure de Kripke grâce à la réduction d'ordre partiel, une technique qui ignore l'ordre de certaines actions du programme. Cela permet de réduire la taille de la structure de Kripke. La seconde méthode modifie la première pour permettre de l'utiliser pour tester des propriétés LTL. La troisième a pour but de vérifier qu'un modèle ne contient pas de livelock, sans utiliser de propriété LTL. Nous testons toutes ces méthodes, en se concentrant sur leur but commun~: réduire la quantité de mémoire requise, ce qui est un goulot d'étranglement important dans le domaine de la vérification de modèles.