Dans ce mémoire nous nous intéressons à une branche de la vérification qui consiste
à comparer une spécification (fonctionnement idéal) à son implémentation (système
réel). Tous les deux sont sous forme de systèmes probabilistes, c’est-à-dire des systèmes
dont le comportement est incertain mais quantifié par des distributions de probabilité.
Il y a plusieurs méthodes disponibles pour comparer les systèmes : la bisimulation, la simulation,
l’équivalence de traces, ou bien les distances qui s’adaptent au comportement
probabiliste auquel nous nous intéressons. En effet, plutôt que de dire si oui ou non les
deux systèmes à comparer sont « équivalents » une distance nous donne une valeur qui
quantifie leur différence. Si la distance est 0 les deux systèmes sont équivalents.
Il y a plusieurs notions de distances pour les systèmes probabilistes, le but de ce
mémoire est de comparer trois d’entre elles : -distance, K-moment et Desharnais et
al. Le principal résultat de cette comparaison est que les trois méthodes ont des résultats
qui ne sont pas fondamentalement différents, bien qu’elles soient conçues de façon
difficilement comparable. Il arrive souvent que les distances se suivent. Les principales
différences se manifestent dans le temps de calcul, la capacité de traitement et l’atténuation
du futur. Nous démontrons que les performances de chaque distance varient
selon le type de système traité. Cela signifie que pour choisir la meilleure méthode, il
faut déterminer le type de système que nous avons. En prenant par exemple un système
dont nous n’avons pas le modèle, c’est la famille K-moment qui sera la seule capable de
calculer une distance. Par ailleurs, nous avons pu intégrer dans la -distance un facteur
qui atténue les différences les plus lointaines par rapport à celles plus proches. Cela
nous a amené à définir une nouvelle distance : -distance atténuée.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2012/28874 |
| Date | 02 1900 |
| Creators | Zhioua, Abir |
| Contributors | Desharnais, Josée, Laviolette, François |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | application/pdf |
| Rights | © Abir Zhioua, 2012 |
Page generated in 0.268 seconds