Análisis y diseño de protocolos de comunicación entre vehículos en un sistema de tránsito modelado como un sistema distribuido.

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