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:LAVAL/oai:corpus.ulaval.ca:20.500.11794/23025 |
| Date | 18 April 2018 |
| Creators | Zhioua, Abir |
| Contributors | Laviolette, François, Desharnais, Josée |
| Source Sets | Université Laval |
| Language | French |
| Detected Language | French |
| Type | mémoire de maîtrise, COAR1_1::Texte::Thèse::Mémoire de maîtrise |
| Format | 99 p., application/pdf |
| Rights | http://purl.org/coar/access_right/c_abf2 |
Page generated in 0.002 seconds