Implémentation des transitions invisibles et transparentes dans Spot

Auteurs

Vincent Tourneur

Type

techreport

Année

2018

Numéro

1809

Résumé

Dans le domaine de la vérification de modèle, la Réduction d'Ordre Partiel (ROP) est une méthode qui permet de réduire notablement la taille des structures de données utilisées pour représenter les différentes exécutions possibles d'un modèle de programme, en considérant seulement les exécutions représentatives. Cela a un coût : de l'information est perdue. Si le but est seulement de vérifier l'absence d'interblocage, il reste assez d'information. Mais en ce qui concerne la vérification de formules LTL, de l'information importante peut-être perdue : les exécutions qui peuvent modifier la valeur de PA (Propositions Atomiques) qui apparaissent dans la formule LTL. De plus, il est seulement possible de vérifier des formules LTL X. Les méthodes des transitions invisibles et transparentes ajoutent des conditions à remplir pendant la ROP, pour garder assez d'information pour la vérification de formule LTL. Nous expliquons le fonctionnement de ces méthodes et leurs implémentations dans la bibliothèque de vérification de modèles Spot.