Resumen

Proponemos una modelización y verificación formal general del sistema de control del tráfico aéreo (ATC). Este estudio se basa en las normas y recomendaciones de la Organización de Aviación Civil Internacional (OACI), la Administración Federal de Aviación (FAA) y la Administración Nacional de Aeronáutica y del Espacio (NASA). Proporciona un sofisticado sistema de asistencia que ayuda a visualizar las aeronaves y presenta detección automática de fallos. En un sistema de seguridad tan crítico, es muy necesario el uso de métodos formales robustos que garanticen la ausencia de errores. Por lo tanto, este trabajo sugiere un formalismo de sistemas de transición discreta basado en la abstracción y el refinamiento a lo largo de las pruebas. Estas garantizan la consistencia del sistema mediante la preservación de invariantes y la ausencia de bloqueos. Por lo tanto, todos los invariantes se mantienen permanentemente, proporcionando una solución práctica para la verificación de ausencia de errores. De ello se deduce que dicha libertad de bloqueo garantiza el funcionamiento continuo de un sistema dado. Esta técnica de especificación y modelado permite corregir el sistema por construcción.

• Materias:Máquina de vectores Estudio numérico Controlador Método computacional Modelado matemático
• Subjects:Vector machine Numerical study Controller Computational method Mathematical modeling
• Palabras claves:sistema, libertad de bloqueo, Organización de Aviación Civil Internacional, sistema de control del tráfico aéreo, Administración Federal de Aviación, detección automática de fallos, verificación de ausencia de fallos, sistema de seguridad crítico, sistemas de transición discreta, modelado formal general
• Keywords:system, deadlock freedom, International Civil Aviation Organization, air traffic control system, Federal Aviation Administration, automatic bugs detection, bugs absence verification, critical safety system, discrete transition systems, general formal modeling