Vérification Formelle Des Protocoles De Communication

Résumé: L'intérêt principal conduisant à l'utilisation des méthodes formelles en général, est de déléguer la détection d'erreurs au programme qui accepte le langage formel, et de réduire ainsi l'occurrence d'erreurs fonctionnelles non détectées habituellement par les réalisateurs humains. Pour les protocoles, la détection d'inconsistances dans la séquence d'échange de messages et la détermination de la vivacité de tous les états possibles est un aspect crucial du développement, étant donné la quantité élevée de messages qu'un protocole utilise habituellement. Dans notre thèse, nous avons proposé un modèle formel pour analyser le protocole d'accès aléatoire dans les réseaux mobiles. Ce modèle consiste d'un réseau d'automates probabilistes communicants. Ce modèle formel sert d'entrée pour l'outil de modèle checking qui réalise une exploration exhaustive de tous les chemins d'exécutions possibles. Cette technique permet de vérifier rigoureusement des propriétés qualitatives telles que la réussite d'envoi du message et le succès de la procédure d'accès aléatoire, mais elle souffre d'un grand handicape, en parle du problème de l'explosion de l'espace d'états qui limite le champ d'application de ces techniques. Ceci a limité cette phase d'étude à un nombre réduit de noeuds du réseau ce qui diverge du cas des réseaux réels où on trouve des centaines d'utilisateurs. Pour pousser notre analyse à des réseaux plus vastes, nous avons opté pour la technique de model checking statistique (SMC) qui un compromis entre l'approche rigoureuse et la simulation. Les résultats d'analyse ont montré les limites du protocole d'une part, et les limite de ces techniques dans ce domaine.

Publié dans la revue: