Return to search

Analyse de diverses distances en vérification formelle probabiliste

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.

Identiferoai:union.ndltd.org:LAVAL/oai:corpus.ulaval.ca:20.500.11794/23025
Date18 April 2018
CreatorsZhioua, Abir
ContributorsLaviolette, François, Desharnais, Josée
Source SetsUniversité Laval
LanguageFrench
Detected LanguageFrench
Typemémoire de maîtrise, COAR1_1::Texte::Thèse::Mémoire de maîtrise
Format99 p., application/pdf
Rightshttp://purl.org/coar/access_right/c_abf2

Page generated in 0.002 seconds