Cadre formel pour le test de robustesse. Application au protocole SSL
Résumé
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. Dans ce document, nous décrivons une méthode pour tester formellement la robustesse d'un système. Nous expliquons comment augmenter la spécification nominale pour prendre en compte les aléas, puis nous formalisons, à travers une relation binaire, la notion de robustesse entre une implémentation sous test et la spécification augmentée. Ensuite, nous expliquons comment générer des séquences de test à partir de cette spécification augmentée. Enfin, nous proposons une étude de cas sur le protocole SSL en utilisant l'outil TGSE pour la génération de séquences de test.
Loading...