Los métodos formales ofrecen medios bien definidos para la verificación matemática de las especificaciones funcionales de los sistemas de software. Para la ingeniería basada en modelos, la verificación de modelos es una técnica de verificación que explora todos los posibles estados del sistema. El Lenguaje de Definición de Escenarios de Aviación es un lenguaje específico de dominio diseñado en base a un proceso de desarrollo de escenarios desde una perspectiva de ingeniería impulsada por modelos. Su objetivo es proporcionar un lenguaje de definición bien estructurado para especificar escenarios de salida, en ruta, desvío y aterrizaje. Este artículo utiliza diagramas de estado y un verificador de modelos para la verificación de cada escenario generado y utiliza ejemplos para demostrar la conformidad con las reglas establecidas en los diagramas de estado para verificar la lógica de todos los escenarios futuros.