Síntesis Unificada de Monitores y Controladores para Asegurar Sistemas Aéreos No Tripulados Complejos
Autores: Yang, Dong; Dong, Wei; Lu, Wei; Liu, Sirui; Dong, Yanqi
Idioma: Inglés
Editor: MDPI
Año: 2025
Acceso abierto
Artículo científico
2025
Síntesis Unificada de Monitores y Controladores para Asegurar Sistemas Aéreos No Tripulados Complejos
Categoría
Ingeniería y Tecnología
Subcategoría
Ingeniería Robótica
Palabras clave
Sistemas de aeronaves no tripuladas
Ataques de seguridad
Verificación en tiempo de ejecución
Síntesis reactiva
Síntesis de controladores
Propiedades de los UAS
Licencia
CC BY-SA – Atribución – Compartir Igual
Consultas: 1
Citaciones: Sin citaciones
Los Sistemas de Aeronaves No Tripuladas (UAS) han experimentado un rápido desarrollo en los últimos años, pero también se han vuelto vulnerables a ataques de seguridad y al entorno externo volátil. Asegurar que el rendimiento de los UAS sea seguro y protegido sin importar cómo cambie el entorno es un desafío. La Verificación en Tiempo de Ejecución (RV) es una técnica de verificación formal ligera que podría utilizarse para monitorear el rendimiento de los UAS y garantizar la seguridad, mientras que la síntesis reactiva es una metodología para sintetizar automáticamente un controlador correcto por construcción. Este documento aborda el problema de la generación y diseño de un controlador seguro para UAS al introducir un método unificado de monitoreo y síntesis de controladores basado en RV y síntesis reactiva. Primero, introducimos un nuevo marco metodológico, en el cual se aplica RV para garantizar diversas propiedades de los UAS, con el controlador reactivo centrado principalmente en la gestión de tareas. Luego, proponemos un patrón de especificación para representar diferentes propiedades de los UAS y generar monitores RV. Además, se propone un método de programación detallado basado en prioridades para programar eventos de monitores y controladores. Además, diseñamos dos métodos basados en la generación de especificaciones y re-síntesis para resolver el problema de la generación de tareas utilizando métricas para la síntesis reactiva. Luego, para facilitar a los usuarios el uso de nuestro método para diseñar controladores seguros para UAS de manera más eficiente, desarrollamos un lenguaje específico de dominio (UAS-DL) para modelar UAS. Finalmente, utilizamos F Prime para implementar nuestro método y realizar experimentos en una plataforma de simulación conjunta. Los resultados experimentales muestran que nuestro método puede generar controladores seguros para UAS, garantizar una mayor seguridad y protección de los UAS, y requerir menos tiempo de síntesis.
Descripción
Los Sistemas de Aeronaves No Tripuladas (UAS) han experimentado un rápido desarrollo en los últimos años, pero también se han vuelto vulnerables a ataques de seguridad y al entorno externo volátil. Asegurar que el rendimiento de los UAS sea seguro y protegido sin importar cómo cambie el entorno es un desafío. La Verificación en Tiempo de Ejecución (RV) es una técnica de verificación formal ligera que podría utilizarse para monitorear el rendimiento de los UAS y garantizar la seguridad, mientras que la síntesis reactiva es una metodología para sintetizar automáticamente un controlador correcto por construcción. Este documento aborda el problema de la generación y diseño de un controlador seguro para UAS al introducir un método unificado de monitoreo y síntesis de controladores basado en RV y síntesis reactiva. Primero, introducimos un nuevo marco metodológico, en el cual se aplica RV para garantizar diversas propiedades de los UAS, con el controlador reactivo centrado principalmente en la gestión de tareas. Luego, proponemos un patrón de especificación para representar diferentes propiedades de los UAS y generar monitores RV. Además, se propone un método de programación detallado basado en prioridades para programar eventos de monitores y controladores. Además, diseñamos dos métodos basados en la generación de especificaciones y re-síntesis para resolver el problema de la generación de tareas utilizando métricas para la síntesis reactiva. Luego, para facilitar a los usuarios el uso de nuestro método para diseñar controladores seguros para UAS de manera más eficiente, desarrollamos un lenguaje específico de dominio (UAS-DL) para modelar UAS. Finalmente, utilizamos F Prime para implementar nuestro método y realizar experimentos en una plataforma de simulación conjunta. Los resultados experimentales muestran que nuestro método puede generar controladores seguros para UAS, garantizar una mayor seguridad y protección de los UAS, y requerir menos tiempo de síntesis.