|
Abstract : |
This thesis describes the development of an automatic generator of backtracking protocol trace analysis tools for single-module specifications written in the formal description language, Estelle. The generated tool automatically checks the validity of any execution trace against the given specification. The approach taken was to modify an Estelle-to-C++ compiler. Discussion about nondeterministic specifications, multiple observation points, and on-line trace analysis follow. Trace analyzers for the protocols LAPD and TP0 have been tested and performance results are evaluated. Issues in the analysis of partial traces are discussed. Ce m'emoire d'ecrit le d'eveloppement d'un g'en'erateur automatique d'outils pour l'analyse de traces de protocoles de communication non-d'eterministes, d'ecrits par des specifications formelles Estelle `a un seul module. L'outil g'en'er'e v'erifie automatiquement la validit'e d'une trace d'ex'ecution par rapport `a la sp'ecification de r'ef'erence. L'approche suivie consistait en la modification d'un compilateur Estelle-C++ existant. Une discussion a propos de specifications non-deterministes, de points d'observation multiples, et d'analyse de traces `a la vol'ee est presentee par la suite. Des analyseurs de traces pour les protocoles LAPD et TP0 ont 'et'e testes, et leurs r'esultats de performance 'evalu'es. Enfin,, |
