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 implementi...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
PeerJ Inc.
2025-01-01
|
| Series: | PeerJ Computer Science |
| Subjects: | |
| Online Access: | https://peerj.com/articles/cs-2575.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841545826410692608 |
|---|---|
| author | Jianyu Zhang Long Zhang Yixuan Wu Linru Ma Feng Yang |
| author_facet | Jianyu Zhang Long Zhang Yixuan Wu Linru Ma Feng Yang |
| author_sort | Jianyu Zhang |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-5a2d82d4f04244cfaa6cb972dcd6f538 |
| institution | Kabale University |
| issn | 2376-5992 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | PeerJ Inc. |
| record_format | Article |
| series | PeerJ Computer Science |
| spelling | doaj-art-5a2d82d4f04244cfaa6cb972dcd6f5382025-01-11T15:05:13ZengPeerJ Inc.PeerJ Computer Science2376-59922025-01-0111e257510.7717/peerj-cs.2575An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiencyJianyu Zhang0Long Zhang1Yixuan Wu2Linru Ma3Feng Yang4School of Automation Engineering, University of Electronic Science and Technology of China, Chengdu, ChinaNational Key Laboratory of Science and Technology on Information System Security, AMS, Beijing, ChinaSchool of Electronics and Information, Northwestern Polytechnical University, Xi’an, ChinaNational Key Laboratory of Science and Technology on Information System Security, AMS, Beijing, ChinaNational Key Laboratory of Science and Technology on Information System Security, AMS, Beijing, ChinaUncrewed 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.https://peerj.com/articles/cs-2575.pdfUncrewed aerial systems (UAS)System reliabilityArchitecture analysis and design language (AADL)Formal verification |
| spellingShingle | Jianyu Zhang Long Zhang Yixuan Wu Linru Ma Feng Yang An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency PeerJ Computer Science Uncrewed aerial systems (UAS) System reliability Architecture analysis and design language (AADL) Formal verification |
| title | An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency |
| title_full | An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency |
| title_fullStr | An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency |
| title_full_unstemmed | An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency |
| title_short | An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency |
| title_sort | integrated modeling verification and code generation for uncrewed aerial systems less cost and more efficiency |
| topic | Uncrewed aerial systems (UAS) System reliability Architecture analysis and design language (AADL) Formal verification |
| url | https://peerj.com/articles/cs-2575.pdf |
| work_keys_str_mv | AT jianyuzhang anintegratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT longzhang anintegratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT yixuanwu anintegratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT linruma anintegratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT fengyang anintegratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT jianyuzhang integratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT longzhang integratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT yixuanwu integratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT linruma integratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency AT fengyang integratedmodelingverificationandcodegenerationforuncrewedaerialsystemslesscostandmoreefficiency |