{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T13:05:48Z","timestamp":1777640748594,"version":"3.51.4"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T00:00:00Z","timestamp":1491955200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T00:00:00Z","timestamp":1491955200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100006195","name":"Ames Research Center","doi-asserted-by":"publisher","award":["NNX14AN61A"],"award-info":[{"award-number":["NNX14AN61A"]}],"id":[{"id":"10.13039\/100006195","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006195","name":"Ames Research Center","doi-asserted-by":"publisher","award":["NNX12AK33A"],"award-info":[{"award-number":["NNX12AK33A"]}],"id":[{"id":"10.13039\/100006195","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10703-017-0275-x","type":"journal-article","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T08:29:09Z","timestamp":1491985749000},"page":"31-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":59,"title":["R2U2: monitoring and diagnosis of security threats for unmanned aerial systems"],"prefix":"10.1007","volume":"51","author":[{"given":"Patrick","family":"Moosbrugger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristin Y.","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johann","family":"Schumann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,12]]},"reference":[{"key":"275_CR1","unstructured":"Adapteva: The parallella board, https:\/\/www.parallella.org\/board"},{"key":"275_CR2","unstructured":"Ahmed A, Lisitsa A, Dixon C (2013) Testid: a high performance temporal intrusion detection system. In: ICIMP 2013, The eighth international conference on internet monitoring and protection, pp 20\u201326"},{"key":"275_CR3","unstructured":"Ardupilot.com: APM:Plane, Open source fixed-wing aircraft UAV, http:\/\/plane.ardupilot.com"},{"key":"275_CR4","doi-asserted-by":"publisher","unstructured":"Bartocci E, Grosu R, Karmarkar A, Smolka SA, Stoller SD, Zadok E, Seyster J (2013) Adaptive runtime verification. In: Proc RV 2012, LNCS, vol 7687. Springer. doi: 10.1007\/978-3-642-35632-2_18","DOI":"10.1007\/978-3-642-35632-2_18"},{"key":"275_CR5","doi-asserted-by":"publisher","unstructured":"Bilge L, Dumitras T (2012) Before we knew it: An empirical study of zero-day attacks in the real world. In: Proceedings of the 2012 ACM conference on computer and communications security. pp 833\u2013844. CCS \u201912, ACM, New York, NY, USA, doi: 10.1145\/2382196.2382284","DOI":"10.1145\/2382196.2382284"},{"key":"275_CR6","unstructured":"Bushnell D, Denney E, Enomoto F, Pai G, Schumann J (2013) Preliminary recommendations for the collection, storage, and analysis of UAS safety data. Technical Report NASA\/TM-2013-216624, NASA Ames Research Center"},{"key":"275_CR7","unstructured":"Chavira M, Darwiche A (2005) Compiling Bayesian networks with local structure. In: Proceedings of the 19th international joint conference on artificial intelligence (IJCAI), pp 1306\u20131312"},{"key":"275_CR8","unstructured":"Christian Science Monitor: RQ-170 GPS Spoofing (2011), http:\/\/www.csmonitor.com\/World\/Middle-East\/2011\/1215\/Exclusive-Iran-hijacked-US-drone-says-Iranian-engineer-Video"},{"key":"275_CR9","doi-asserted-by":"publisher","unstructured":"Donz\u00e9 A, Maler O, Bartocci E, Nickovic D, Grosu R, Smolka S (2012) On temporal logic and signal processing. In: Proc ATVA 2012, LNCS, vol 7561. Springer. doi: 10.1007\/978-3-642-33386-6_9","DOI":"10.1007\/978-3-642-33386-6_9"},{"key":"275_CR10","doi-asserted-by":"publisher","unstructured":"Fisher K (2014) Using formal methods to enable more secure vehicles: DARPA\u2019s HACMS program. In: Proceedings of the 19th ACM SIGPLAN international conference on functional programming. pp 1\u20131. ICFP \u201914, ACM, New York, NY, USA, doi: 10.1145\/2628136.2628165","DOI":"10.1145\/2628136.2628165"},{"key":"275_CR11","unstructured":"GAO (2015) Air traffic control: FAA needs a more comprehensive approach to address cybersecurity as agency transitions to nextgen. Tech. Rep. GAO-15-370, United States Government Accountability Office (04 2015), http:\/\/www.gao.gov\/assets\/670\/669627.pdf"},{"key":"275_CR12","doi-asserted-by":"publisher","unstructured":"Geist J, Rozier KY, Schumann J (2014) Runtime observer pairs and bayesian network reasoners on-board FPGAs: Flight-certifiable system health management for embedded systems. In: Proceedings of Runtime verification - 5th international conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Springer, pp 215\u2013230. doi: 10.1007\/978-3-319-11164-3_18","DOI":"10.1007\/978-3-319-11164-3_18"},{"issue":"5","key":"275_CR13","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1049\/iet-sen.2013.0236","volume":"8","author":"D Heffernan","year":"2014","unstructured":"Heffernan D, Macnamee C, Fogarty P (2014) Runtime verification monitoring for automotive embedded systems using the iso 26262 functional safety standard as a guide for the definition of the monitored properties. IET Softw 8(5):193\u2013203","journal-title":"IET Softw"},{"key":"275_CR14","unstructured":"Humphreys T (2012) Statement on the vulnerability of civil unmanned aerial vehicles and other systems to civil GPS spoofing. University of Texas at Austin (July 18, 2012)"},{"key":"275_CR15","doi-asserted-by":"publisher","first-page":"12702","DOI":"10.1155\/2012\/127072","volume":"2012","author":"A Jafarnia-Jahromi","year":"2012","unstructured":"Jafarnia-Jahromi A, Broumandan A, Nielsen J, Lachapelle G (2012) GPS vulnerability to spoofing threats and a review of antispoofing techniques. Int J Navig Obs 2012:12702. doi: 10.1155\/2012\/127072","journal-title":"Int J Navig Obs"},{"key":"275_CR16","doi-asserted-by":"crossref","unstructured":"Jaksic S, Bartocci E, Grosu R, Kloibhofer R, Nguyen T, Nickovic D (2015) From signal temporal logic to FPGA monitors. In: 2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp 218\u2013227","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"275_CR17","doi-asserted-by":"crossref","unstructured":"Javaid AY, Sun W, Devabhaktuni VK, Alam M (2012) Cyber security threat analysis and modeling of an unmanned aerial vehicle system. In: Proceedings of international conference on technologies for Homeland security (HST), 2012 IEEE, pp 585\u2013590","DOI":"10.1109\/THS.2012.6459914"},{"key":"275_CR18","unstructured":"JSBSim: JSBSim - open source flight dynamics model, http:\/\/jsbsim.sourceforge.net"},{"key":"275_CR19","doi-asserted-by":"crossref","unstructured":"Kalajdzic K, Bartocci E, Smolka SA, Stoller SD, Grosu R (2013) Runtime verification with particle filtering. In: Proc RV 2013, LNCS, vol 8174. Springer, pp 149\u2013166","DOI":"10.1007\/978-3-642-40787-1_9"},{"issue":"4","key":"275_CR20","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1002\/rob.21513","volume":"31","author":"AJ Kerns","year":"2014","unstructured":"Kerns AJ, Shepard DP, Bhatti JA, Humphreys TE (2014) Unmanned aircraft capture and control via GPS spoofing. J Field Robot 31(4):617\u2013636","journal-title":"J Field Robot"},{"key":"275_CR21","doi-asserted-by":"publisher","unstructured":"Kim A, Wampler B, Goppert J, Hwang I, Aldridge H (2012) Cyber attack vulnerabilities analysis for unmanned aerial vehicles. In: Proceedings of Infotech@Aerospace 2012. doi: 10.2514\/6.2012-2438","DOI":"10.2514\/6.2012-2438"},{"issue":"4","key":"275_CR22","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-time Syst 2(4):255\u2013299","journal-title":"Real-time Syst"},{"key":"275_CR23","doi-asserted-by":"crossref","unstructured":"Kwon C, Liu W, Hwang I (2013) Security analysis for cyber-physical systems against stealthy deception attacks. In: 2013 American control conference, pp 3344\u20133349","DOI":"10.1109\/ACC.2013.6580348"},{"key":"275_CR24","unstructured":"Lu H, Forin A (2007) The design and implementation of P2V, an architecture for zero-overhead online verification of software programs. Tech. Rep. MSR-TR-2007-99, Microsoft Research, http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=70470"},{"key":"275_CR25","doi-asserted-by":"crossref","unstructured":"Magiera J, Katulski R (2015) Detection and mitigation of GPS spoofing based on antenna array processing. J Appl Res Technol 13(1): 45\u201357, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1665642315300043","DOI":"10.1016\/S1665-6423(15)30004-3"},{"key":"275_CR26","doi-asserted-by":"publisher","unstructured":"Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Pillars of Computer Science, LNCS, vol 4800. Springer, pp 475\u2013505. doi: 10.1007\/978-3-540-78127-1_26","DOI":"10.1007\/978-3-540-78127-1_26"},{"key":"275_CR27","unstructured":"MAVProxy: A UAV ground station software package for mavlink based systems, http:\/\/tridge.github.io\/MAVProxy"},{"key":"275_CR28","unstructured":"McMilin E, De Lorenzo DS, Walter T, Lee TH, Enge P (2014) Single antenna GPS spoof detection that is simple, static, instantaneous and backwards compatible for aerial applications. In: Proceedings of the 27th international technical meeting of the satellite division of the institute of navigation (ION GNSS+ 2014), Tampa, FL. pp 2233\u20132242"},{"issue":"5","key":"275_CR29","doi-asserted-by":"publisher","first-page":"874","DOI":"10.1109\/TSMCA.2010.2052037","volume":"40","author":"OJ Mengshoel","year":"2010","unstructured":"Mengshoel OJ, Chavira M, Cascio K, Poll S, Darwiche A, Uckun S (2010) Probabilistic model-based diagnosis: an electrical power system case study. IEEE Trans Syst Man Cyberne Part A Syst Hum 40(5):874\u2013885","journal-title":"IEEE Trans Syst Man Cyberne Part A Syst Hum"},{"issue":"3","key":"275_CR30","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2012","unstructured":"Meredith PO, Jin D, Griffith D, Chen F, Ro\u015fu G (2012) An overview of the MOP runtime verification framework. Int J Softw Tools Technol Transf 14(3):249\u2013289","journal-title":"Int J Softw Tools Technol Transf"},{"key":"275_CR31","doi-asserted-by":"crossref","unstructured":"Musliner D, Hendler J, Agrawala AK, Durfee E, Strosnider JK, Paul CJ (1995) The challenges of real-time AI. IEEE Computer 28, 58\u201366. http:\/\/citeseer.comp.nus.edu.sg\/article\/musliner95challenges.html","DOI":"10.1109\/2.362628"},{"key":"275_CR32","doi-asserted-by":"crossref","unstructured":"Naldurg P, Sen K, Thati P (2004) A temporal logic based framework for intrusion detection. In: FORTE, LNCS, vol. 3235, Springer, pp 359\u2013376","DOI":"10.1007\/978-3-540-30232-2_23"},{"key":"275_CR33","doi-asserted-by":"crossref","unstructured":"Olivain J, Goubault-Larrecq J (2005) The orchids intrusion detection tool. In: CAV, LNCS, vol. 3576, Springer, pp 286\u2013290","DOI":"10.1007\/11513988_28"},{"key":"275_CR34","unstructured":"Pearl J (1985) A constraint propagation approach to probabilistic reasoning. In: UAI, AUAI Press, pp 31\u201342"},{"key":"275_CR35","doi-asserted-by":"crossref","unstructured":"Pellizzoni R, Meredith P, Caccamo M, Rosu G (2008) Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: RTSS 2008, IEEE, pp 481\u2013491","DOI":"10.1109\/RTSS.2008.43"},{"key":"275_CR36","unstructured":"Perry S (2015) Subcommittee hearing: Unmanned aerial system threats: exploring security implications and mitigation technologies. Committee on homeland security, http:\/\/homeland.house.gov\/hearing\/subcommittee-hearing-unmanned-aerial-system-threats-exploring-security-implications-and"},{"key":"275_CR37","doi-asserted-by":"crossref","unstructured":"Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: Proc RV 2010, LNCS, vol 6418, Springer, pp 345\u2013359","DOI":"10.1007\/978-3-642-16612-9_26"},{"issue":"6","key":"275_CR38","doi-asserted-by":"publisher","first-page":"1258","DOI":"10.1109\/JPROC.2016.2526658","volume":"104","author":"ML Psiaki","year":"2016","unstructured":"Psiaki ML, Humphreys TE (2016) GNSS spoofing and detection. Proc IEEE 104(6):1258\u20131270","journal-title":"Proc IEEE"},{"key":"275_CR39","doi-asserted-by":"crossref","unstructured":"Reinbacher T, Geist J, Moosbrugger P, Horauer M, Steininger A (2012) Parallel runtime verification of temporal properties for embedded software. In: MESA, pp 224\u2013231","DOI":"10.1109\/MESA.2012.6275566"},{"key":"275_CR40","unstructured":"Reinbacher T (2013) Analysis of embedded real-time systems at runtime. Ph.D. thesis, Technische Universit\u00e4t Wien, Austria"},{"key":"275_CR41","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.scico.2012.10.015","volume":"80","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher T, Brauer J, Horauer M, Steininger A, Kowalewski S (2014) Runtime verification of microcontroller binary code. Sci Comput Program 80:109\u2013129. doi: 10.1016\/j.scico.2012.10.015","journal-title":"Sci Comput Program"},{"key":"275_CR42","doi-asserted-by":"publisher","unstructured":"Reinbacher T, Rozier KY, Schumann J (2014) Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Tools and algorithms for the construction and analysis of systems - 20th international conference, TACAS 2014, Grenoble, France, LNCS, vol 8413, pp 357\u2013372. Springer. doi: 10.1007\/978-3-642-54862-8_24","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"275_CR43","doi-asserted-by":"crossref","unstructured":"Schumann J, Mbaya T, Mengshoel OJ, Pipatsrisawat K, Srivastava A, Choi A, Darwiche A (2013) Software health management with Bayesian networks. In: Innovations in System and Software Engineering, vol 9. Springer, pp 271\u2013292","DOI":"10.1007\/s11334-013-0214-y"},{"key":"275_CR44","doi-asserted-by":"publisher","unstructured":"Schumann J, Moosbrugger P, Rozier KY (2015) R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Proc RV 2015, LNCS, vol 9333. Springer, Cham. pp 233\u2013249. doi: 10.1007\/978-3-319-23820-3_15","DOI":"10.1007\/978-3-319-23820-3_15"},{"key":"275_CR45","doi-asserted-by":"crossref","unstructured":"Schumann J, Roychoudhury I, Kulkarni C (2015) Diagnostic reasoning using prognostic information for unmanned aerial systems. In: Proceedings of the 2015 annual conference of the prognostics and health management society (PHM2015)","DOI":"10.36001\/phmconf.2015.v7i1.2548"},{"key":"275_CR46","doi-asserted-by":"crossref","unstructured":"Schumann J, Rozier KY, Reinbacher T, Mengshoel OJ, Mbaya T, Ippolito C (2013) Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. In: Proceedings of the 2013 annual conference of the prognostics and health management society (PHM2013)","DOI":"10.36001\/phmconf.2013.v5i1.2275"},{"issue":"21","key":"275_CR47","first-page":"1","volume":"6","author":"J Schumann","year":"2015","unstructured":"Schumann J, Rozier KY, Reinbacher T, Mengshoel OJ, Mbaya T, Ippolito C (2015) Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. Int J Progn Health Manag 6(21):1\u201327","journal-title":"Int J Progn Health Manag"},{"key":"275_CR48","doi-asserted-by":"crossref","unstructured":"Selyunin K, Nguyen T, Bartocci E, Nickovic D, Grosu R (2016) Monitoring of MTL specifications with IBM\u2019s spiking-neuron model. In: 2016 Design, automation test in europe conference exhibition (DATE), pp 924\u2013929","DOI":"10.3850\/9783981537079_0139"},{"key":"275_CR49","doi-asserted-by":"publisher","unstructured":"Selyunin K, Nguyen T, Bartocci E, Grosu R (2016) Applying runtime monitoring for automotive electronic development. In: Proc RV 2016, LNCS, vol 10012. Springer, pp 462\u2013469. doi: 10.1007\/978-3-319-46982-9_30","DOI":"10.1007\/978-3-319-46982-9_30"},{"key":"275_CR50","unstructured":"Shachtman N, Axe D Most U.S. drones openly broadcast secret video feeds. Wired (10 2012), http:\/\/www.wired.com\/2012\/10\/hack-proof-drone\/"},{"issue":"8","key":"275_CR51","first-page":"30","volume":"23","author":"DP Shepard","year":"2012","unstructured":"Shepard DP, Bhatti JA, Humphreys TE (2012) Drone hack. GPS World 23(8):30\u201333","journal-title":"GPS World"},{"key":"275_CR52","doi-asserted-by":"publisher","unstructured":"Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2012) Runtime verification with state estimation. In: Proc RV 2011, LNCS, vol 7186. Springer, pp 193\u2013207. doi: 10.1007\/978-3-642-29860-8_15","DOI":"10.1007\/978-3-642-29860-8_15"},{"key":"275_CR53","doi-asserted-by":"publisher","unstructured":"Todman T, Stilkerich S, Luk W (2015) In-circuit temporal monitors for runtime verification of reconfigurable designs. In: Proceedings of the 52nd annual design automation conference. pp 50:1\u201350:6. DAC \u201915, ACM, New York, NY, USA, doi: 10.1145\/2744769.2744856","DOI":"10.1145\/2744769.2744856"},{"key":"275_CR54","unstructured":"U.S. Air Force: Aircraft Accident Investigation: RQ-1L, S\/N 96-3023. AIB Class A Aerospace mishaps (September 2000), http:\/\/usaf.aib.law.af.mil\/ExecSum2000\/RQ-1L_Nellis_14Sep00.pdf"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0275-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0275-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0275-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T14:54:22Z","timestamp":1719154462000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0275-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,12]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["275"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0275-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,12]]},"assertion":[{"value":"12 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}