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

TL;DR

This paper presents an integrated approach using AADL for modeling, verifying, and generating code for UAS, improving safety and efficiency in designing reliable unmanned aerial systems.

Contribution

It introduces a comprehensive method combining modeling, formal verification, and code generation for UAS using AADL, which is novel in streamlining development and ensuring safety.

Findings

Effective early vulnerability detection in UAS design

Successful automatic generation of flight controller code

Enhanced efficiency in UAS development process

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.