Kavli Affiliate: Long Zhang
| First 5 Authors: Jianyu Zhang, Long Zhang, Yixuan Wu, Linru Ma, Feng Yang
| Summary:
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.
| Search Query: ArXiv Query: search_query=au:”Long Zhang”&id_list=&start=0&max_results=3