Jump to : Abstract | Contact | BibTex reference | EndNote reference |
Le développement de logiciels dans le domaine des réseaux et des machines à mémoire distribuée n'est pas encore bien maîtrisé du fait de la répartition des ressources. Il existe donc un besoin en matière de méthodes et d'outils permettant de fiabiliser ces logiciels répartis. La validation de protocoles est un des moyens de relever ce défi, mais, si les travaux théoriques sont nombreux, trop peu sont réellement applicables à de vrais outils. Nous présentons dans ce document nos travaux dans le domaine de la validation de protocoles dont la ligne de conduite principale est la possibilité de transfert vers de vrais outils de validation. Dans une première partie, nous traitons du problème de l'infinitude du graphe d'accessibilité de spécifications de protocoles communiquant par files fifo. Le problème étant indécidable, nous cherchons une condition suffisante la plus générale possible. Cette condition fournit une procédure de test d'infinitude applicable à toutes les spécifications du modèle. Malgré cette approche par le test, nous démontrons que cette procédure améliore les résultats de décidabilité existants. En outre, nous montrons que ce test peut être appliqué à des spécification Estelle, ce qui le rend utilisable dans un vrai outil de vérification. Nous apportons ensuite une contribution au problème de l'explosion combinatoire des graphes d'accessibilité finis. Certaines propriétés peuvent être vérifiées pendant le parcours de ces graphes. Nous décrivons donc un algorithme de parcours en profondeur à remplacement aléatoire qui utilise une mémoire bornée, dont la taille est insuffisante pour conserver tout le graphe, mais suffisante pour un parcours exhaustif. Nous donnons les résultats que nous avons obtenus en expérimentant cet algorithme dans un prototype d'outil de validation. Puis nous traitons de l'utilisation du parcours avec remplacement dans la vérification "à la volée" pour la validation d'une spécification par un automate de Büchi, la bisimulation de systèmes de transitions, le test d'infinitude et la vérification d'autres propriétés d'accessibilité. Enfin nous présentons nos idées sur la conception d'un outil de validation dont l'algorithme de base serait un parcours en profondeur à remplacement aléatoire. Nous présentons les structures de données permettant une gestion efficace et au moindre coût des contenus de files fifo. Pour conclure, nous insistons sur les possibilités de transfert des algorithmes présentés dans le document, certains d'entre-eux étant déjà à l'étude. Nous présentons quelques perspectives sur l'extension du test d'infinitude à d'autres problèmes d'accessibilité et sur les possibilités d'utilisation du parcours avec remplacement.
Thierry Jéron
Thierry.Jeron@irisa.fr
@PhdThesis{Jeron-These-91,
Author = {Jéron, T.},
Title = {Contribution à la validation des protocoles : test d'infinitude et vérification à la volée},
School = {Université de Rennes I},
Month = {May},
Year = {1991}
}
Get EndNote Reference (.ref)