Model checking: un modelo del protocolo Gnutella

Abstract

En este trabajo se presenta una especificación del protocolo de comunicación Gnutella para redes Peer-to-Peer. Se realizó un modelo de este protocolo utilizando SPIN, un sistema de verificación automática que incluye algoritmos de comprobación de modelos. Se presentan dos modelos: uno completo, apropiado para la simulación del comportamiento de un nodo Gnutella, y otro acotado, que permite comprobar si determinadas propiedades expresadas en LTL (Lógica Temporal Lineal) son ciertas. A manera de ejemplo, dos fórmulas fueron comprobadas en el modelo con el fin de verificarlas.

This paper presents a specification of the Gnutella communication protocol for Peer-to-Peer networks. A model of this protocol has been made using SPIN, an automatic verification system which includes model-checking algorithms. Two models are presented: a complete one, suitable for simulating the behavior of a Gnutella node; and a limited one, which allows checking whether certain properties expressed in LTL (Linear Temporal Logic) are true. As example, two formulas have been checked in this model to verify them.