LIP6 2002/025

• Rapports de recherche
  Validation Formelle du protocole ZCSP avec SPIN
• V. Beaudenon, E. Encrenaz, J.-L. Desbarbieux
• 8 pages - 27/01/2003- document en - http://www.lip6.fr/lip6/reports/2002/lip6.2002.025.pdf - 194 Ko
• Contact : Vincent.Beaudenon (at) nulllip6.fr
• Ancien Thème : ASIM
Nous nous intéressons au problème de modélisation et de validation d'un protocole de type "zéro-copie". Le protocole ZCSP (Zero-Copy secured protocol) est basé sur un accès direct en mémoire. Nous avons procédé à deux approches : un modèle couvrant un ensemble fini de séquences afin d'en mesurer la robustesse. Le second modèle étant plus proche de la réalité. Nous décrivons aussi les propriétés validées. Les espaces de recherche atteignant des tailles prohibitives, nous expliquerons quelles réductions nous avons faites.
• Mots clés : Validation de modèles, SPIN, ProMeLa, ZCSP, LTL
• Directeur de la publication : Francois.Dromard (at) nulllip6.fr