Towards a fomral Approach of Communication Protocols through Refinement and Proofs

Abstract

Différentes approches ont été utilisées pour la spécification formelle et la vérification des protocoles de communication. L’approche considérée dans ce travail se concentre sur la vérification déductive dans laquelle la correction d’un modèle par déduction se ramène à la preuve de formules mathématiques appelées obligations de preuve. Dans notre approche, nous avons choisi la méthode Event-B. Event-B est un langage de spécification formel, elle offre un potentiel élevé en termes de correction grâce à son mécanisme de raffinement bien connu, de ses obligations de preuve bien définies et de la plate-forme RODIN. Notre objectif été de construire un modèle avec une formulation claire et précise des propriétés liées aux protocoles de communication et de décharger toutes les obligations de preuve. Pour cela, nous partons d'exigences abstraites, nous les raffinons progressivement pour obtenir une description concrète et détaillée du modèle et nous vérifions chaque niveau de raffinement par rapport à la spécification construite dans le raffinement précédent. Ce qui va nous permettre de vérifier la correction, c'est-à-dire la préservation des propriétés de l'étape précédente, par rapport aux raffinements successifs. Ceci est atteint par la création et la démonstration de logique.