Abstract:
Azimir et al. en el trabajo de investigación Manejo de Intersecciones utilizando Redes Vehiculares propone el protocolo MP-IP, destinado para la comunicación entre vehículos autónomos en intersecciones; el objetivo de este protocolo es aumentar la seguridad y rendimiento en el tráfico. Los resultados de este protocolo muestran que el uso del protocolo aumenta el rendimiento del tráfico en un 83% comparado con el sistema de luces tradicional. Sin embargo, es importante garantizar la confiabilidad de este protocolo para evitar posibles daños materiales o humanos en su implementación en un escenario real.
En el presente trabajo se aplica el método de Verificación de modelos al protocolo MP-IP con el fin de verificar que el diseño de MP-IP es correcto bajo un modelo y propiedades formales. Para modelar el diseño del protocolo se utilizó el lenguaje de verificación de modelos PROMELA, además, se plante´o un conjunto de propiedades que el protocolo debe cumplir para verificar su correctitud; estas propiedades fueron planteadas formalmente utilizando Lógica Temporal Lineal. Las propiedades fueron verificadas por medio de la herramienta SPIN, adicionalmente se verificó la ausencia de bloqueo mutuo y código inalcanzable en el protocolo utilizando esta herramienta.
Finalmente, los resultados de SPIN mostraron que el protocolo cumple con las propiedades planteadas, es libre de bloqueo muto y código inalcanzable. Por lo tanto, el protocolo MP-IP es correcto bajo esa especificación. RR
