Verificação de projetos de controle de veículos aéreos autônomos

Abstract

Flight systems formal checking became necessary once automatic control systems became widely applied, as they are complex, interdisciplinary and have highly dependent components. Failures are resposible from financial to human lives’ losses. Expansion of automatic control systems application enables market innovations such as Unmanned Aerial Vehicles (UAV) for passenger transport. Commercial deployment of UAV gets restricted by commercial barriers which can be diminished or removed by validating related designs. This impacts in accident reduction as well as in presenting trust arguments for passengers. Commonly used techniques such as simulation and testing are proven incomplete and may not detect serious errors. Flight systems’ formal checking, even though being necessary for fullfilling flight industries formal requiremments, is scarce due to its complexity and computational cost. Flight system models for airflight systems verification tools benchmark sets are also scarce. This work presents a synthetic model set Simulink implementation built of complex airflight systems abstractions. Thirteen components are presented, classified as target, tracking, guidance and airframe systems having modular composition for complete systems building. Three complete model compositions are presented and simulated. This work also analyzes airflight systems’ verification problem from the model’s study and development to its translation and verification. For that, this work presents SMCT, a translator for models described in Simulink language to XMV language. SMCT presents improvements over other Simulink processing tools that overcome difficulties on textual source code syntax/semantics analysis. Applying SMCT, this work translates and verifies implemented models using NuXMV tool, validating modeled functionalities. An operational law set is also checked as an example of the technique application. Results are a positive pointer on complex systems’ verification as autonomous flight, especially through different domain automatic techniques association, which reduces experts multidisciplinarity requirements for models failure checking. This work offers a starting toolset for commercial barriers’ reduction through airflight systems formal checking described in a widely used language.