Difference between revisions of "Publications/tourneur.18.seminar/fr"
From LRDE
(Created page with "{{CSIReportFR | authors = Vincent Tourneur | titre = Implementation des Transitions Invisibles et Transparantes dans Spot | year = 2018 | number = 1809 | resume = Dans le doma...") |
|||
| Line 1: | Line 1: | ||
{{CSIReportFR |
{{CSIReportFR |
||
| authors = Vincent Tourneur |
| authors = Vincent Tourneur |
||
| − | | titre = |
+ | | titre = Implémentation des Transitions Invisibles et Transparentes dans Spot |
| year = 2018 |
| year = 2018 |
||
| number = 1809 |
| number = 1809 |
||
Revision as of 15:45, 8 June 2018
- 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.