{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T09:40:21Z","timestamp":1736415621640,"version":"3.32.0"},"reference-count":28,"publisher":"PeerJ","license":[{"start":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T00:00:00Z","timestamp":1736380800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.7717\/peerj-cs.2575","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T08:58:36Z","timestamp":1736413116000},"page":"e2575","source":"Crossref","is-referenced-by-count":0,"title":["An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency"],"prefix":"10.7717","volume":"11","author":[{"given":"Jianyu","family":"Zhang","sequence":"first","affiliation":[{"name":"School of Automation Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Long","family":"Zhang","sequence":"additional","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, AMS, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yixuan","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Electronics and Information, Northwestern Polytechnical University, Xi\u2019an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linru","family":"Ma","sequence":"additional","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, AMS, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feng","family":"Yang","sequence":"additional","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, AMS, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"4443","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"issue":"4","key":"10.7717\/peerj-cs.2575\/ref-1","doi-asserted-by":"publisher","first-page":"1518","DOI":"10.3390\/s21041518","article-title":"Sensors and measurements for unmanned systems: an overview","volume":"21","author":"Balestrieri","year":"2021","journal-title":"Sensors"},{"issue":"4","key":"10.7717\/peerj-cs.2575\/ref-2","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods: state of the art and future directions","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"10.7717\/peerj-cs.2575\/ref-3","article-title":"Secure mathematically-assured composition of control models","author":"Cofer","year":"2017"},{"issue":"1","key":"10.7717\/peerj-cs.2575\/ref-4","doi-asserted-by":"publisher","first-page":"106727","DOI":"10.1016\/j.ast.2021.106727","article-title":"RFlySim: automatic test platform for UAV autopilot systems with FPGA-based hardware-in-the-loop simulations","volume":"114","author":"Dai","year":"2021","journal-title":"Aerospace Science and Technology"},{"key":"10.7717\/peerj-cs.2575\/ref-5","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1109\/DSN.2019.00027","article-title":"SOTER: a runtime assurance framework for programming safe robotics systems","author":"Desai","year":"2019"},{"key":"10.7717\/peerj-cs.2575\/ref-6","first-page":"1","article-title":"Open source AADL tool environment (OSATE)","author":"Feiler","year":"2004"},{"key":"10.7717\/peerj-cs.2575\/ref-7","doi-asserted-by":"crossref","DOI":"10.21236\/ADA455842","article-title":"The architecture analysis & design language (AADL): an introduction","author":"Feiler","year":"2006"},{"key":"10.7717\/peerj-cs.2575\/ref-8","article-title":"Unmanned and autonomous systems of systems test and evaluation: challenges and opportunities","author":"Ferreira","year":"2010"},{"issue":"2104","key":"10.7717\/peerj-cs.2575\/ref-9","doi-asserted-by":"publisher","first-page":"20150401","DOI":"10.1098\/rsta.2015.0401","article-title":"The HACMS program: using formal methods to eliminate exploitable bugs","volume":"375","author":"Fisher","year":"2017","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"issue":"3","key":"10.7717\/peerj-cs.2575\/ref-10","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2692956.2663177","article-title":"Resolute: an assurance case language for architecture models","volume":"34","author":"Gacek","year":"2014","journal-title":"ACM SIGAda Ada Letters"},{"issue":"4","key":"10.7717\/peerj-cs.2575\/ref-11","doi-asserted-by":"publisher","first-page":"1646","DOI":"10.2139\/ssrn.3451039","article-title":"Review of unmanned aircraft system (UAS)","volume":"2","author":"Gupta","year":"2013","journal-title":"International Journal of Advanced Research in Computer Engineering & Technology (IJARCET)"},{"key":"10.7717\/peerj-cs.2575\/ref-12","doi-asserted-by":"publisher","first-page":"106885","DOI":"10.1016\/j.ress.2020.106885","article-title":"Failure mode and effect analysis improvement: a systematic literature review and future research Agenda","volume":"199","author":"Huang","year":"2020","journal-title":"Reliability Engineering & System Safety"},{"issue":"8","key":"10.7717\/peerj-cs.2575\/ref-13","doi-asserted-by":"publisher","first-page":"7346763","DOI":"10.1155\/2020\/7346763","article-title":"Formal verification of hardware components in critical systems","volume":"2020","author":"Khan","year":"2020","journal-title":"Wireless Communications and Mobile Computing"},{"key":"10.7717\/peerj-cs.2575\/ref-14","first-page":"141","article-title":"Reliable generation of formal specifications using large language models","author":"Kogler","year":"2024"},{"key":"10.7717\/peerj-cs.2575\/ref-15","first-page":"279","article-title":"Runtime assurance based on formal specifications","author":"Lee","year":"1999"},{"key":"10.7717\/peerj-cs.2575\/ref-16","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2405.02580","article-title":"PropertyGPT: LLM-driven formal verification of smart contracts through retrieval-augmented property generation","author":"Liu","year":"2024"},{"issue":"2","key":"10.7717\/peerj-cs.2575\/ref-17","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1177\/1748006X211034970","article-title":"Using formal methods for autonomous systems: five recipes for formal verification","volume":"237","author":"Luckcuck","year":"2023","journal-title":"Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability"},{"issue":"1","key":"10.7717\/peerj-cs.2575\/ref-18","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/32.825767","article-title":"A classification and comparison framework for software architecture description languages","volume":"26","author":"Medvidovic","year":"2000","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.7717\/peerj-cs.2575\/ref-19","first-page":"6235","article-title":"PX4: a node-based multithreaded open source robotics framework for deeply embedded platforms","author":"Meier","year":"2015"},{"issue":"1","key":"10.7717\/peerj-cs.2575\/ref-20","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s11370-022-00452-4","article-title":"Unmanned aerial vehicles (UAVs): practical aspects, applications, open challenges, security issues, and future trends","volume":"16","author":"Mohsan","year":"2023","journal-title":"Intelligent Service Robotics"},{"key":"10.7717\/peerj-cs.2575\/ref-21","first-page":"5255","article-title":"Onboard deep-learning-based unmanned aerial vehicle fault cause detection and identification","author":"Sadhu","year":"2020"},{"issue":"12","key":"10.7717\/peerj-cs.2575\/ref-22","doi-asserted-by":"publisher","first-page":"2205","DOI":"10.2514\/1.G004862","article-title":"Runtime assurance for autonomous aerospace systems","volume":"43","author":"Schierman","year":"2020","journal-title":"Journal of Guidance, Control, and Dynamics"},{"issue":"1","key":"10.7717\/peerj-cs.2575\/ref-23","doi-asserted-by":"publisher","first-page":"26","DOI":"10.3390\/robotics10010026","article-title":"Unmanned aerial drones for inspection of offshore wind turbines: a mission-critical failure analysis","volume":"10","author":"Shafiee","year":"2021","journal-title":"Robotics"},{"issue":"10","key":"10.7717\/peerj-cs.2575\/ref-24","doi-asserted-by":"publisher","first-page":"14081","DOI":"10.1007\/s12652-022-04113-3","article-title":"A novel fault diagnosis in sensors of quadrotor unmanned aerial vehicle","volume":"14","author":"Taimoor","year":"2023","journal-title":"Journal of Ambient Intelligence and Humanized Computing"},{"issue":"4","key":"10.7717\/peerj-cs.2575\/ref-25","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1109\/MNET.001.1900546","article-title":"Unmanned systems security: models, challenges, and future directions","volume":"34","author":"Tan","year":"2020","journal-title":"IEEE Network"},{"issue":"2","key":"10.7717\/peerj-cs.2575\/ref-26","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1177\/2041304110394727","article-title":"Autonomous vehicle control systems\u2014a review of decision making","volume":"225","author":"Veres","year":"2011","journal-title":"Proceedings of the Institution of Mechanical Engineers, Part I: Journal of Systems and Control Engineering"},{"issue":"2","key":"10.7717\/peerj-cs.2575\/ref-27","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/MS.2012.173","article-title":"Your \u201cwhat\u201d is my \u201chow\u201d: iteration and hierarchy in system design","volume":"30","author":"Whalen","year":"2012","journal-title":"IEEE Software"},{"key":"10.7717\/peerj-cs.2575\/ref-28","doi-asserted-by":"publisher","first-page":"107","DOI":"10.5194\/isprsarchives-XXXVIII-1-C22-107-2011","article-title":"Real-time monitoring system using unmanned aerial vehicle integrated with sensor observation service","volume":"38","author":"Witayangkurn","year":"2012","journal-title":"The International Archives of the Photogrammetry, Remote Sensing and Spatial Information Sciences"}],"container-title":["PeerJ Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/peerj.com\/articles\/cs-2575.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/peerj.com\/articles\/cs-2575.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/peerj.com\/articles\/cs-2575.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/peerj.com\/articles\/cs-2575.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T08:58:50Z","timestamp":1736413130000},"score":1,"resource":{"primary":{"URL":"https:\/\/peerj.com\/articles\/cs-2575"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,9]]},"references-count":28,"alternative-id":["10.7717\/peerj-cs.2575"],"URL":"https:\/\/doi.org\/10.7717\/peerj-cs.2575","archive":["CLOCKSS","LOCKSS","Portico"],"relation":{},"ISSN":["2376-5992"],"issn-type":[{"value":"2376-5992","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,9]]},"article-number":"e2575"}}