Difference between revisions of "Publications/huvelle.19.seminar/fr"
From LRDE
Line 4: | Line 4: | ||
| year = 2019 |
| year = 2019 |
||
| number = 1906 |
| number = 1906 |
||
− | | resume = Spot peut gerer les automates testeurs depuis Spot 1.0. Cependant, Spot 2.0 introduit une nouvelle structure de |
+ | | resume = Spot est une bibliothèque d'algorithmes de vérification de modèles qui peut gérer plusieurs types d'automate omega. Spot peut aussi gerer les automates testeurs depuis Spot 1.0. Cependant, Spot 2.0 a introduit une nouvelle structure de donnée pour les automates avec des conditions d'acceptance génériques et qui n'était pas disponible quand les automates testeurs ont été implémenté. Notre but est de réimplémenter les automates testeurs en utilisant cette nouvelle structure de donnée. Cela fait, nous esperons pouvoir réutiliser les algorithms existantsreduire la quantité de code impliquant les automates testeurs et de rendre les automates testeurs compatible avec le format HOA. Pour finirl'implémentation choisi permettrait de reduire la taille des automates testeurs comparé à l'implémentation originale. |
| type = techreport |
| type = techreport |
||
| id = huvelle.19.seminar |
| id = huvelle.19.seminar |
Revision as of 19:54, 27 June 2019
- Auteurs
- Martin Huvelle
- Type
- techreport
- Année
- 2019
- Numéro
- 1906
Résumé
Spot est une bibliothèque d'algorithmes de vérification de modèles qui peut gérer plusieurs types d'automate omega. Spot peut aussi gerer les automates testeurs depuis Spot 1.0. Cependant, Spot 2.0 a introduit une nouvelle structure de donnée pour les automates avec des conditions d'acceptance génériques et qui n'était pas disponible quand les automates testeurs ont été implémenté. Notre but est de réimplémenter les automates testeurs en utilisant cette nouvelle structure de donnée. Cela fait, nous esperons pouvoir réutiliser les algorithms existantsreduire la quantité de code impliquant les automates testeurs et de rendre les automates testeurs compatible avec le format HOA. Pour finirl'implémentation choisi permettrait de reduire la taille des automates testeurs comparé à l'implémentation originale.