Communication protocols for web services

Abstract

Dans le domaine des Services Web les protocoles de communication peuvent être modélisés sous forme de communication d’automates d’états finis (CAEF). Bien que les automates d’états finis permettent une bonne modélisation de Services, ils n’offrent pas une vue de différents niveaux dans le cas de protocoles complexes. L’utilisation des modèles de communication d’automates d’états finis complexes (CAEFC) introduit de la modularité et de la hiérarchie sur la spécification de protocoles, permettant ainsi d’avoir une meilleure modélisation. Avant d’implémenter un protocole nous devons vérifier sa correction car une modélisation de protocole peut avoir quelques problèmes qui se traduisent par des erreurs de protocole, comme les erreurs d’interblocage et les transitions non exécutables. Donc, vérifier qu’un protocole ne contient pas des erreurs revient à valider sa spécification. L’opération de validation consiste à vérifier que tous les états du graphe d’accessibilité (d’exécution) de protocole ne présentent pas des erreurs logiques. L’introduction des automates complexes nécessite la définition d’une technique de validation qui supporte de tel modèle et qui réduit la complexité de son analyse. Dans ce mémoire, nous proposons une technique de validation de protocoles modélisés sous forme de CAEFC, appelée RLRA (Reverse Leaping Reachability Analysis). Notre technique, permet la détection de toutes les erreurs de type interblocage dans une spécification de protocole. En se basant sur une approche de validation avec retour arrière, on commence par identifier de possibles états d’interblocage ensuite, valider parmi ces états suspects, ceux qui présentent réellement une erreur à travers la recherche des chemins de retours vers la racine du graphe de protocole. Pour réduire le problème de l’explosion combinatoire, nous introduisons les graphes de sauts (leap graphe) que nous exploitons dans la construction des chemins de retour arrière, ce qui apporte une réduction importante sur la taille du graphe à parcourir. Ce travail est terminé par un ensemble de tests et de comparaisons à fin de montrer l’efficacité de la technique proposée.