Presentation / Exposé :
La génération de tests pour les protocoles à l'aide
de la technologie de la vérification
Colloque sur l'application des méthodes formelles au
développement des systèmes critiques. 17, 18, 19
Janvier
Grenoble
Fichier PostScript (222K)
Claude Jard. Pampa/IRISA/CNRS
Le test est un aspect important du cycle de développement d'un
logiciel, et particulièrement dans le domaine des protocoles, vu la
difficulté intrinsèque de leur conception. Tester, c'est essayer de
s'assurer que l'implantation fait bien ce que l'on attend d'elle. Pour
donner un sens précis aux verdicts du test, il faut donc décrire
soigneusement ce que l'implantation est censée faire: c'est le rôle
de la spécification formelle. Nous nous plaçons dans le cadre d'une
approche formalisée dans laquelle l'activité de test est définie par un
modèle mathématique (les systèmes de transitions) qui permet de décrire
les spécifications, les implantations, la notion de conformité et la
procédure de test. La technique de génération automatique de tests est
fondée sur une analyse sémantique de la spécification formelle du
système à tester. Cette analyse est guidée par la donnée d'un objectif
de test. L'objectif de test représente une description abstraite du test
à générer. La méthode vérifie que l'objectif est valide, dans le sens
où le test correspondant fournira un diagnostic fiable, et génère un arbre
de test, qui, une fois appliqué à l'implantation, fournit un verdict
``pass'', ``fail'', ou ``inconclusive''. Les transformations successives
de la spécification (renversement, abstraction, pose des verdicts et des
timers) sont intégrées dans le calcul à la volée du système de transitions
associé à la spécification. L'exposé décrira aussi l'expérience de développement d'un prototype, appelé TGV, à l'intérieur de l'outil
Open-Caesar, en collaboration avec l'équipe Spectre, et le résultat de
son utilisation sur des spécifications LDS de services RNIS militaires,
en partenariat avec Vérilog, Cap-Sesa-Régions et le Cnet.