Integrated Modeling, Verification, and Code Generation for Unmanned Aerial Systems

TL;DR

UAS safety-critical systems face increasing complexity and development costs. The authors propose an integrated workflow that couples AADL-based modeling with AGREE/Resolute verification and automated flight controller code generation, executed within the OSATE environment. The approach yields generic UAS models, formal safety proofs for key functions, and generated PX4-compatible code from verified models, enabling early vulnerability detection and efficient code production. Experimental results indicate improved reliability and development efficiency with reduced verification costs, highlighting the method's practical impact for high-reliability UAS design.

Abstract

Unmanned Aerial Systems (UAS) are currently widely used in safety-critical fields such as industrial production, military operations, and disaster relief. Due to the diversity and complexity of application scenarios, UAS have become increasingly intricate. The challenge of designing and implementing highly reliable UAS while effectively controlling development costs and enhancing efficiency is a pressing issue faced by both academia and industry. Addressing this challenge, this paper aims to investigate an integrated approach to modeling, verification, and code generation for UAS. The paper begins by utilizing Architecture Analysis and Design Language (AADL) to model the UAS, proposing a set of generic UAS models. Based on these models, formal specifications are written to describe the system's safety properties and functions. Finally, the paper introduces a method for generating flight controller code for UAS based on the verified models. Experiments conducted with the proposed method demonstrate its effectiveness in identifying potential vulnerabilities in the UAS during the early design phase and in generating viable flight controller code from the verified models. This approach can enhance the efficiency of designing and verifying high-reliability UAS.

Figures (16)

• Figure 1: Overall framework of the method.
• Figure 2: Top-level component structure.
• Figure 3: Flight controller system component structure.
• Figure 4: Model overall structure diagram.
• Figure 5: Subcomponent ARM_Cortex_M7 properties and interfaces.