logo móvil
Contáctanos

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

Descargar PDF

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


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.

Otros recursos que podrían interesarte

Temas Virtualpro