Cadre Formel pour le Test de Robustesse des Protocoles de Communication

Abstract

Dans le domaine des télécommunications, il est indispensable de valider rigoureusement les protocoles avant de les mettre en service. Ainsi, il faut non seulement tester la conformité d'un protocole, mais il s'avère aussi nécessaire de tester sa robustesse face àdes événements imprévus. La littérature concernant le test de robustesse est beaucoup moins conséquente que le test de conformité. A travers ce document, nous considérons la définition de la robustesse suivante : "la capacité d'un système, conforme à sa spécification nominale, à adopter un comportement acceptable en présence d'aléas". Notre approche se fonde sur l'analyse du comportement du système face à des aléas. On considérera comme aléa tout événement non prévu amenant le système à une impossibilité temporaire ou définitive d'exécuter une action. Les contributions principales de ce document sont brièvement présentées ci-dessous :() Proposition d'un cadre formel comportant une approche, une relation de robustesse et méthode pour générer les cas de test de robustesse d'un système modélisé sous forme d'IOLTS. Notre approche comporte deux méthodes :- La méthode TRACOR (Test de Robustesse en présence d'Aléas COntrôlables et Représentables) consiste à vérifier la robustesse d'un système en présence d'aléas contrôlables et représentables. Cette méthode intègre les entrées invalides, entrées inopportunes, sortiesacceptables et traces de blocage dans la spécification nominale, pour obtenir une spécification augmentée. Cette dernière servira de base pour la génération de séquences de test de robustesse.- La méthode TRACON (Test de Robustesse en présence d'Aléas COntrôlables et Non représentables) est focalisée sur le test de robustesse en présence d'aléas contrôlables et non représentables. Elle consiste à enrichir la spécification nominale par les sorties acceptables et les traces de suspension afin d'obtenir la spécification semi-augmentée. Cette dernière servira de base pour la génération de séquences de test de robustesse.(2) Pour formaliser la robustesse d'une implémentation vis-à-vis de la spécification augmentée (ou la spécification semi-augmentée), nous proposons une relation binaire, appelée "Robust", basée sur l'observation des sorties et blocages de l'implémentation après l'exécution de traces comportant les aléas.(3) Afin de générer les cas de test de robustesse, nous proposons une méthode basée sur un coloriage de la spécification augmentée (ou la spécification semi-augmentée) et un ensemble d'objectifs de test de robustesse.(4) Les fondements de notre approche sont implémentés dans l'outil RTCG. Cette application offre trois interfaces. La première et la deuxième permettent d'automatiser la méthode TRACOR. La troisième interface permet d'automatiser la méthode TRACON.(5) Une étude de cas, sur les protocoles SSL handshake et TCP, montrant une évaluationpratique de notre approche.