Retour à la page du séminaire

9/04/99: Jean-François Monin (CNET, Lannion)
vérification formelle d'un algorithme normalisé de contrôle de conformité ATM : bilan de quelques expériences et perspectives pour les méthodes formelles

résumé

L'une des clefs pour assurer la qualité de service (QoS) dans les réseaux large bande est la réservation préalable des ressources : il est alors possible de garantir à l'utilisateur la QoS qu'il a demandée pourvu que son trafic respecte les engagements négociés en début de connexion. Un composant crucial dans le réseau est donc le dispositif qui vérifie la conformité des cellules qui entrent. Dans le cas de la classe de QoS dite ABR, ce dispositif est régi par un algorithme court mais non trivial : il est l'aboutissement de plusieurs mois d'efforts des instances de normalisation, qui se sont conclus avec la preuve formelle réalisée au CNET. Par la suite, ce problème a été soumis a différents laboratoires afin d'évaluer différents outils de vérification et de comprendre la nature des difficultés posées. On fera dans l'exposé un bilan de ces différentes approches et outils, comprenant Gap, Hytech, MEC, B, Coq et Spike.