Enfoque de modelado de UPPAAL para una estrategia basada en autómatas temporizados para controlar el acceso de drones a zonas críticas
Autores: Krichen, Moez
Idioma: Inglés
Editor: MDPI
Año: 2024
Acceso abierto
Artículo científico
2024
Enfoque de modelado de UPPAAL para una estrategia basada en autómatas temporizados para controlar el acceso de drones a zonas críticas
Categoría
Ingeniería y Tecnología
Subcategoría
Ingeniería Eléctrica y Electrónica
Palabras clave
Acceso
Drones
Zona crítica
Autómatas temporizados
UPPAAL
Estrategia
Licencia
CC BY-SA – Atribución – Compartir Igual
Consultas: 36
Citaciones: Sin citaciones
Controlar el acceso a zonas críticas mediante drones es crucial para garantizar la seguridad y operaciones eficientes en diversas aplicaciones. En esta investigación, proponemos una estrategia para controlar el acceso de un conjunto de drones a una zona crítica utilizando autómatas temporizados y UPPAAL. UPPAAL es un verificador de modelos y simulador para sistemas en tiempo real, que permite el modelado, simulación y verificación de autómatas temporizados. Nuestro sistema consta de seis drones, un controlador y un buffer, todos modelados como autómatas temporizados. Presentamos un modelo formal que captura el comportamiento e interacciones de estos componentes, considerando las restricciones de permitir solo un dron en la zona crítica a la vez. Los autómatas temporizados son un formalismo poderoso para modelar y analizar sistemas en tiempo real, ya que pueden capturar los aspectos temporales del comportamiento del sistema. Las ventajas de utilizar autómatas temporizados incluyen la capacidad de modelar sistemas críticos en tiempo, analizar propiedades de seguridad y vivacidad, y verificar la corrección del sistema. Diseñamos una estrategia que implica señalizar a los drones que se acercan, prevenir colisiones y garantizar un acceso ordenado a la zona crítica. Utilizamos UPPAAL para simular y verificar el sistema, incluida la evaluación de propiedades como propiedades de validación, propiedades de seguridad, propiedades de vivacidad y ausencia de bloqueos. Sin embargo, una limitación de los autómatas temporizados es que pueden volverse complejos y difíciles de modelar para sistemas a gran escala, y el análisis puede ser computacionalmente costoso a medida que aumenta el número de componentes y comportamientos. A través de simulaciones y verificación formal, demostramos la efectividad y corrección de nuestra estrategia propuesta. Los resultados resaltan la capacidad de los autómatas temporizados y UPPAAL para proporcionar un análisis confiable y riguroso de los sistemas de control de acceso de drones. Nuestra investigación contribuye al desarrollo de estrategias sólidas y seguras para gestionar las operaciones de drones en zonas críticas.
Descripción
Controlar el acceso a zonas críticas mediante drones es crucial para garantizar la seguridad y operaciones eficientes en diversas aplicaciones. En esta investigación, proponemos una estrategia para controlar el acceso de un conjunto de drones a una zona crítica utilizando autómatas temporizados y UPPAAL. UPPAAL es un verificador de modelos y simulador para sistemas en tiempo real, que permite el modelado, simulación y verificación de autómatas temporizados. Nuestro sistema consta de seis drones, un controlador y un buffer, todos modelados como autómatas temporizados. Presentamos un modelo formal que captura el comportamiento e interacciones de estos componentes, considerando las restricciones de permitir solo un dron en la zona crítica a la vez. Los autómatas temporizados son un formalismo poderoso para modelar y analizar sistemas en tiempo real, ya que pueden capturar los aspectos temporales del comportamiento del sistema. Las ventajas de utilizar autómatas temporizados incluyen la capacidad de modelar sistemas críticos en tiempo, analizar propiedades de seguridad y vivacidad, y verificar la corrección del sistema. Diseñamos una estrategia que implica señalizar a los drones que se acercan, prevenir colisiones y garantizar un acceso ordenado a la zona crítica. Utilizamos UPPAAL para simular y verificar el sistema, incluida la evaluación de propiedades como propiedades de validación, propiedades de seguridad, propiedades de vivacidad y ausencia de bloqueos. Sin embargo, una limitación de los autómatas temporizados es que pueden volverse complejos y difíciles de modelar para sistemas a gran escala, y el análisis puede ser computacionalmente costoso a medida que aumenta el número de componentes y comportamientos. A través de simulaciones y verificación formal, demostramos la efectividad y corrección de nuestra estrategia propuesta. Los resultados resaltan la capacidad de los autómatas temporizados y UPPAAL para proporcionar un análisis confiable y riguroso de los sistemas de control de acceso de drones. Nuestra investigación contribuye al desarrollo de estrategias sólidas y seguras para gestionar las operaciones de drones en zonas críticas.