Resumen:
Planificación de trayectorias en vehículos autónomos ha sido abordada en numerosas ocasiones y con diversos enfoques. Es una problemática que involucra un cambio de estado o traslado. Consiste en proporcionar una trayectoria que satisfaga una serie de requerimientos mediante un mapa (entrada del sistema) y un conjunto de restricciones (determinadas por el comportamiento deseado del sistema). Estas restricciones pueden ser: puntos, obstáculos y otros requerimientos. La planificación de trayectorias puede ser vista también como un problema de control donde se modifica la posición de un sistema haciendo uso de variables de entorno, donde los datos de entrada serán nuestras claves para contextualizar el sistema y en consecuencia generar una ruta que cumpla con las especificaciones. Planificación de trayectorias tiene varias aplicaciones en robótica, vehículos aéreos, desarrollo de aplicaciones, etc.
En este trabajo abordaremos una propuesta de solución a la planificación de trayectorias mediante verificación de modelos, la cual propone otra forma de toma de decisiones con base en la abstracción de un mapa y restricciones. Esta verificación consta de: dado un modelo abstracto y dado las propiedades requeridas, determina si las propiedades se cumplen en algún punto del modelo. El verificador de modelos comprobará si la negación de la expresión lógica se cumple o no en el modelo. Este contraejemplo representa una trayectoria dentro del mapa que satisface las restricciones.
En este proyecto se describe la implementación de un algoritmo de planificación de trayectorias para vehículos aéreos, basado en verificación de modelos. Se implementó un ambiente virtual para la visualización de la ejecución de la ruta generada por verificación de modelos; así como la prueba del algoritmo, ya que mediante el mapa dibujado en el ambiente virtual se pueden generar un sinfín de puntos a visitar por el vehículo aéreo, así como, permite visualizar su ejecución.
