面向无人机系统的集成建模、验证与代码生成
Integrated Modeling, Verification, and Code Generation for Unmanned Aerial Systems
AI总结：
本文提出基于 AADL 的 UAS 集成建模、形式化验证和飞行控制器代码生成方法，可在设计早期发现脆弱点并生成可行代码，提升高可靠系统开发效率。
摘要：
无人机系统（UAS）目前广泛应用于工业生产、军事行动和救灾等安全攸关领域。由于应用场景的多样性和复杂性，UAS 正变得日益复杂。如何设计并实现高可靠的 UAS，同时有效控制开发成本并提升效率，是学术界和工业界共同面临的紧迫问题。为应对这一挑战，本文旨在研究一种面向 UAS 的建模、验证与代码生成集成方法。论文首先使用架构分析与设计语言（Architecture Analysis and Design Language，AADL）对 UAS 进行建模，提出一组通用的 UAS 模型。在这些模型的基础上，编写形式化规约以描述系统的安全属性和功能。最后，论文介绍了一种基于已验证模型生成 UAS 飞行控制器代码的方法。使用所提方法开展的实验表明，该方法能够在设计早期有效识别 UAS 中的潜在脆弱点，并能够从已验证模型生成可行的飞行控制器代码。该方法可以提高高可靠 UAS 的设计与验证效率。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
