{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T11:40:27Z","timestamp":1769859627080,"version":"3.49.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031265631","type":"print"},{"value":"9783031265648","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-26564-8_9","type":"book-chapter","created":{"date-parts":[[2023,6,30]],"date-time":"2023-06-30T06:03:11Z","timestamp":1688104991000},"page":"253-282","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Using an Interactive Theorem Prover for Formally Analyzing the Dynamics of the Unmanned Aerial Vehicles"],"prefix":"10.1007","author":[{"given":"Adnan","family":"Rashid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sa\u2019ed","family":"Abed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,1]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Abed SE, Rashid A, Hasan O (2022) Formal analysis of unmanned aerial vehicles using higher-order-logic theorem proving: project webpage. http:\/\/save.seecs.nust.edu.pk\/fauav\/","DOI":"10.1186\/s13634-022-00882-3"},{"issue":"9","key":"9_CR2","first-page":"481","volume":"17","author":"S Abed","year":"2020","unstructured":"Abed S, Rashid A, Hasan O (2020) Formal analysis of unmanned aerial vehicles using higher-order-logic theorem proving. J Aerosp Inf Syst 17(9):481\u2013495","journal-title":"J Aerosp Inf Syst"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Ahmad A, Samad AM (2010) Aerial mapping using high resolution digital camera and unmanned aerial vehicle for geographical information system. In: International colloquium on signal processing and its applications. IEEE, pp 1\u20136","DOI":"10.1109\/CSPA.2010.5545303"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Ar\u00e9chiga N, Loos SM, Platzer A, Krogh BH (2012) Using theorem provers to guarantee closed-loop system properties. In: American control conference. IEEE, pp 3573\u20133580","DOI":"10.1109\/ACC.2012.6315388"},{"key":"9_CR5","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press"},{"issue":"3","key":"9_CR6","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.ijtst.2017.02.001","volume":"5","author":"EN Barmpounakis","year":"2016","unstructured":"Barmpounakis EN, Vlahogianni EI, Golias JC (2016) Unmanned aerial aircraft systems for transportation engineering: current practice and future challenges. Int J Transp Sci Technol 5(3):111\u2013122","journal-title":"Int J Transp Sci Technol"},{"issue":"1","key":"9_CR7","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10846-011-9546-8","volume":"64","author":"A Birk","year":"2011","unstructured":"Birk A, Wiggerich B, B\u00fclow H, Pfingsthorn M, Schwertfeger S (2011) Safety, security, and rescue missions with an unmanned aerial vehicle (UAV). J Intell Robot Syst 64(1):57\u201376","journal-title":"J Intell Robot Syst"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Carreno V, Mu\u00f1oz C (2000) Aircraft trajectory modeling and alerting algorithm verification. In: Theorem proving in higher order logics. LNCS, vol 1869. Springer, pp 90\u2013105","DOI":"10.1007\/3-540-44659-1_6"},{"key":"9_CR9","unstructured":"Chan M, Ricketts D, Lerner S, Malecha G (2016) Formal verification of stability properties of cyber-physical systems. In: Coq for programming languages"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Chen X, Chen G (2018) Formal verification of helicopter automatic landing control algorithm in theorem prover Coq. Int J Performab Eng 14(9)","DOI":"10.23940\/ijpe.18.09.p2.19471957"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Clarke EM, Zuliani P (2011) Statistical model checking for cyber-physical systems. In: Automated technology for verification and analysis. LNCS, vol 6996. Springer, pp 1\u201312","DOI":"10.1007\/978-3-642-24372-1_1"},{"key":"9_CR12","unstructured":"Cook MV (2012) Flight dynamics principles: a linear systems approach to aircraft stability and control. Butterworth-Heinemann"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Cooper J, Goodrich MA (2008) Towards combining UAV and sensor operator roles in UAV-enabled visual search. In: Human robot interaction. ACM, pp 351\u2013358","DOI":"10.1145\/1349822.1349868"},{"issue":"1","key":"9_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis LA, Fisher M, Webster MP, Bordini RH (2012) Model checking agent programming languages. Autom Softw Eng 19(1):5\u201363","journal-title":"Autom Softw Eng"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Ducard GJ (2009) Fault-tolerant flight control and guidance systems: practical methods for small unmanned aerial vehicles. Springer Science & Business Media","DOI":"10.1007\/978-1-84882-561-1"},{"issue":"2008","key":"9_CR16","first-page":"1187","volume":"37","author":"J Everaerts","year":"2008","unstructured":"Everaerts J et al (2008) The use of unmanned aerial vehicles (UAVs) for remote sensing and mapping. Int Arch Photogramm Remote Sens Spat Inf Sci 37(2008):1187\u20131192","journal-title":"Int Arch Photogramm Remote Sens Spat Inf Sci"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Foster T, Bowman J (2005) Dynamic stability and handling qualities of small unmanned-aerial vehicles. In: AIAA aerospace sciences meeting and exhibit, p 1023","DOI":"10.2514\/6.2005-1023"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Gallington RW, Berman H, Entzminger J, Francis MS, Palmore P, Stratakes J (1997) Unmanned aerial vehicles. In: Future aeronautical and space systems, AIAA, progress in astronautics and aeronautics, vol 172, pp 251\u2013295","DOI":"10.2514\/5.9781600866449.0251.0295"},{"issue":"10","key":"9_CR19","first-page":"702","volume":"11","author":"K Ghorbal","year":"2014","unstructured":"Ghorbal K, Jeannin JB, Zawadzki E, Platzer A, Gordon GJ, Capell P (2014) Hybrid theorem proving of aerospace systems: applications and challenges. J Aerosp Inf Syst 11(10):702\u2013713","journal-title":"J Aerosp Inf Syst"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Groza A, Letia IA, Goron A, Zaporojan S (2015) A formal approach for identifying assurance deficits in unmanned aerial vehicle software. In: Progress in systems engineering, vol 366. Springer, pp 233\u2013239","DOI":"10.1007\/978-3-319-08422-0_35"},{"issue":"2","key":"9_CR21","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1080\/01969722.2016.1263513","volume":"48","author":"HM Guzey","year":"2017","unstructured":"Guzey HM (2017) Hybrid consensus-based formation control of fixed-wing MUAVs. Cybern Syst 48(2):71\u201383","journal-title":"Cybern Syst"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Harrison J (1996) HOL light: a tutorial introduction. In: Formal methods in computer-aided design. LNCS, vol 1166. Springer, pp 265\u2013269","DOI":"10.1007\/BFb0031814"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press","DOI":"10.1017\/CBO9780511576430"},{"key":"9_CR24","unstructured":"Harrison J et\u00a0al (1996) Formalized mathematics. Technical report\u00a036, Turku Centre for Computer Science, Finland"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Hasan O, Tahar S (2015) Formal verification methods. In: Encyclopedia of information science and technology. IGI Global Publication, pp 7162\u20137170","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"issue":"9","key":"9_CR26","doi-asserted-by":"publisher","first-page":"1779","DOI":"10.1080\/00207179.2014.889853","volume":"87","author":"A Karimoddini","year":"2014","unstructured":"Karimoddini A, Lin H, Chen BM, Lee TH (2014) Hierarchical hybrid modelling and control of an unmanned helicopter. Int J Control 87(9):1779\u20131793","journal-title":"Int J Control"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Loos SM, Renshaw D, Platzer A (2013) Formal verification of distributed aircraft controllers. In: International conference on hybrid systems: computation and control. ACM, pp 125\u2013130","DOI":"10.1145\/2461328.2461350"},{"issue":"3","key":"9_CR28","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1109\/MIM.2004.1337910","volume":"7","author":"DH Lyon","year":"2004","unstructured":"Lyon DH (2004) A military perspective on small unmanned aerial vehicles. Instrum Measur Mag 7(3):27\u201331","journal-title":"Instrum Measur Mag"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Ma Z, Chen G (2017) Formal derivation and verification of coordinate transformations in theorem prover Coq. In: International conference on dependable systems and their applications, pp 127\u2013136","DOI":"10.1109\/DSA.2017.29"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Malecha G, Ricketts D, Alvarez MM, Lerner S (2016) Towards foundational verification of cyber-physical systems. In: Science of security for cyber-physical systems. IEEE, pp 1\u20135","DOI":"10.1109\/SOSCYPS.2016.7580000"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Munoz C, Narkawicz A (2016) Formal analysis of extended well-clear boundaries for unmanned aircraft. In: NASA formal methods symposium. LNCS, vol 9690. Springer, pp 221\u2013226","DOI":"10.1007\/978-3-319-40648-0_17"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Munoz C, Narkawicz A, Hagen G, Upchurch J, Dutle A, Consiglio M, Chamberlain J (2015) DAIDALUS: detect and avoid alerting logic for unmanned systems. In: Digital avionics systems conference. IEEE, pp 5A1\u20131\u20135A1\u201312","DOI":"10.1109\/DASC.2015.7311421"},{"issue":"2","key":"9_CR33","first-page":"209","volume":"17","author":"A Narkawicz","year":"2012","unstructured":"Narkawicz A, Munoz C (2012) Formal verification of conflict detection algorithms for arbitrary trajectories. Reliable Comput 17(2):209\u2013237","journal-title":"Reliable Comput"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Paulson LC (1996) ML for the working programmer. Cambridge University Press","DOI":"10.1017\/CBO9780511811326"},{"key":"9_CR35","unstructured":"Ping JTK, Ling AE, Quan TJ, Dat CY (2012) Generic unmanned aerial vehicle (UAV) for civilian application-a feasibility assessment and market survey on civilian application for aerial imaging. In: Sustainable utilization and development in engineering and technology. IEEE, pp 289\u2013294"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Seibel CW, Farines JM, Cury JE (1997) Towards using hybrid automata for the mission planning of unmanned aerial vehicles. In: International hybrid systems workshop. LNCS, vol 1567. Springer, pp 324\u2013340","DOI":"10.1007\/3-540-49163-5_18"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Shim D, Kim H, Sastry S (2000) Hierarchical control system synthesis for rotorcraft-based unmanned aerial vehicles. In: AIAA guidance, navigation, and control conference and exhibit, pp 1\u20139","DOI":"10.2514\/6.2000-4057"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Valavanis KP (2008) Advances in unmanned aerial vehicles: state of the art and the road to autonomy. Springer Science & Business Media","DOI":"10.1007\/978-1-4020-6114-1"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Webster M, Fisher M, Cameron N, Jump M (2011) Formal methods for the certification of autonomous unmanned aircraft systems. In: Computer safety, reliability, and security, LNPSE, vol 6894. Springer, pp 228\u2013242","DOI":"10.1007\/978-3-642-24270-0_17"},{"key":"9_CR40","unstructured":"Williams KW (2004) A summary of unmanned aircraft accident\/incident data: human factors implications. Technical report, Federal Aviation Administration"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Xu\u00a0Jr K (2014) Frequency domain system identification of fixed-wing unmanned aerial vehicles","DOI":"10.1155\/2014\/748940"}],"container-title":["Studies in Computational Intelligence","Mobile Robot: Motion Control and Path Planning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-26564-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,30]],"date-time":"2023-06-30T06:12:16Z","timestamp":1688105536000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-26564-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031265631","9783031265648"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-26564-8_9","relation":{},"ISSN":["1860-949X","1860-9503"],"issn-type":[{"value":"1860-949X","type":"print"},{"value":"1860-9503","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"1 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}