Trabalho em anais de evento

Safe UAV Continuous-Control Architecture Design

BECKER, L. B.; GONCALVES, F. S.; BROERING, E. F.; MISSON, H. A.; CORDEIRO, L. C

2024 • 3rd ADEPT workshop: AADL by its practitioners • 1 citações

Resumo

Unmanned Aerial Vehicles (UAVs) are often classified as safety-critical systems due to the severe implications a failure might have. Ensuring safety guarantees is therefore paramount in UAV design. This paper introduces a solution to provide safety guarantees during the design of the continuous-control architecture, a critical component. Formal verification (FV) techniques are employed to detect software errors and verify the architecture's ability to meet real-time system requirements. The first verification round utilizes the ESBMC model checker, focusing on individual elements of the architecture, particularly the continuous-control algorithm. The second verification process employs the UPPAAL model checker to conduct a schedulability analysis of the proposed architecture. Finally, a runtime monitoring analysis is performed using the newly developed RMLib tool. This approach was successfully applied in the design process of a UAV, identifying and correcting various design and implementation issues, as detailed in the paper.

palavras-chave

Palavras-chave

unmanned aerial vehiclesUAV safetyformal verificationUPPAALschedulability analysisruntime monitoringreal-time systemssafety-critical systemssoftware defect detection

Status

Published

links