An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency

Uncrewed Aerial Systems (UASs) are widely implemented in safety-critical fields such as industrial production, military operations, and disaster relief. Due to the diversity and complexity of implementation scenarios, UASs have become increasingly intricate. The challenge of designing and implementing highly reliable UASs while effectively controlling development costs and improving efficiency has been a pressing issue faced by academia and industry. To address this challenge, this article aims to examine an integrated method for modeling, verification, and code generation for UASs. This article begins to utilize Architecture Analysis and Design Language (AADL) to model UASs, proposing generic UAS models. Then, formal specifications describe a system's safety properties and functions based on these models. Finally, this article introduces a method to generate flight controller codes for UASs based on the verified models. Experiments demonstrate its effectiveness in pinpointing potential vulnerabilities in UASs during the early design phase and generating viable flight controller codes from the verified models. The proposed approach can also improve the efficiency of designing and verifying high-reliability UASs.