Modélisations et vérification d'un algorithme temporisé

Jean-François Monin

France Télécom R & D

Lannion, France

Résumé: Les algorithmes de contrôle de conformité de l'ATM protègent le fonctionnement du réseau en retirant les cellules en excès par rapport au trafic négocié dans la connexion courante. Dans le cas du protocole ABR, cela implique un calcul compliqué qui s'effectue en gérant un petit échéancier en temps réel. La normalisation de l'ABR a nécessité une modélisation et une preuve de correction d'abord effectuée à la main puis affinée sous Coq. D'autres modélisations ont été effectuées au moyen d'automates temporisés traditionnels. Les travaux actuels du projet RNRT Calife donnent un cadre unifié à ces expériences et permettent d'aborder des systèmes temporisés beaucoup plus conséquents, comme les protocoles de diffusion multicast de l'IETF.

Back to schedule.

Nicolas Magaud

Last modified: Mon Apr 23 11:06:45 MEST 2001