{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T17:16:27Z","timestamp":1763226987060,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,7,14]],"date-time":"2021-07-14T00:00:00Z","timestamp":1626220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,7,14]],"date-time":"2021-07-14T00:00:00Z","timestamp":1626220800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1552934","CNS-1257011"],"award-info":[{"award-number":["CNS-1552934","CNS-1257011"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","award":["ECF-2016"],"award-info":[{"award-number":["ECF-2016"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"crossref","award":["80NSSC21M0121"],"award-info":[{"award-number":["80NSSC21M0121"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s11334-021-00407-5","type":"journal-article","created":{"date-parts":[[2021,7,14]],"date-time":"2021-07-14T12:03:54Z","timestamp":1626264234000},"page":"567-580","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Integrating runtime verification into an automated UAS traffic management system"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0340-0160","authenticated-orcid":false,"given":"Abigail","family":"Hammer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Cauwels","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Hertz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phillip H.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristin Y.","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,14]]},"reference":[{"key":"407_CR1","unstructured":"AeroViroment: VAPOR All-electric Helicopter UAS (2019) https:\/\/www.avinc.com\/uas\/view\/vapor-vtol . Last Accessed on Dec. 17"},{"issue":"1","key":"407_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Henzinger TA (1993) Real-time logics: complexity and expressiveness. Inf Comput 104(1):35\u201377","journal-title":"Inf Comput"},{"key":"407_CR3","unstructured":"Aweiss AS, Owens BD, Rios JL, Homola JR, Mohlenbrink CP (2018) UAS traffic management national campaign II. In: 2018 AIAA SciTech, pp 1\u201316"},{"key":"407_CR4","doi-asserted-by":"publisher","unstructured":"Basin D, Dardinier T, Heimes L, Krstic S, Raszyk M, Schneider J, Traytel D (2020) A formally verified. https:\/\/doi.org\/10.1007\/978-3-030-51074-9_25","DOI":"10.1007\/978-3-030-51074-9_25"},{"key":"407_CR5","doi-asserted-by":"publisher","DOI":"10.1145\/2699444","author":"D Basin","year":"2015","unstructured":"Basin D, Klaedtke F, Muller S, Salinescu E (2015) Monitoring metric first-order temporal properties. J Assoc Comput Mach. https:\/\/doi.org\/10.1145\/2699444","journal-title":"J Assoc Comput Mach"},{"key":"407_CR6","doi-asserted-by":"publisher","unstructured":"Ben-David S, Chechik M, Gurfinkel A, Uchitel S (2011) Cssl: A logic for specifying conditional scenarios. In: SIGSOFT\/FSE 2011\u2014Proceedings of the 19th ACM SIGSOFT symposium on foundations of software engineering, Association for Computing Machinery, pp 37\u201347. https:\/\/doi.org\/10.1145\/2025113.2025123","DOI":"10.1145\/2025113.2025123"},{"key":"407_CR7","doi-asserted-by":"publisher","unstructured":"Cornell University: Symbolic LTLf Synthesis (2017). https:\/\/doi.org\/10.24963\/ijcai.2017\/189","DOI":"10.24963\/ijcai.2017\/189"},{"key":"407_CR8","unstructured":"Cornell University (2019) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation, vol abs\/1901.06108"},{"key":"407_CR9","unstructured":"Federal Aviation Administration (FAA) (2019) FAA Aerospace Forecast\u2014Fiscal Years 2019\u20132039. Online:https:\/\/www.faa.gov\/data_research\/aviation\/aerospace_forecasts\/media\/FY2019-39_FAA_Aerospace_Forecast.pdf"},{"key":"407_CR10","unstructured":"Federal Aviation Administration (FAA) (2020) Unmanned Aerial Systems (UAS). Online: https:\/\/www.faa.gov\/uas\/"},{"key":"407_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_5","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner B, Gieseking M, Hecking-Harbusch J (2020) AdamMC: a model checker for petri nets with transits against flow-LTL. Comput Aided Verif. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_5","journal-title":"Comput Aided Verif"},{"key":"407_CR12","doi-asserted-by":"crossref","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: RV14, vol 8734, pp 215\u2013230. Springer","DOI":"10.1007\/978-3-319-11164-3_18"},{"key":"407_CR13","doi-asserted-by":"publisher","unstructured":"Havelund K, Peled D (2018) Runtime verification: from propositional to first-order temporal logic. In: Proceedings of 18th international conference, RV 2018, Limassol, Cyprus, November 10\u201313, 2018, pp 90\u2013112. Springer International Publishing. https:\/\/doi.org\/10.1007\/978-3-030-03769-7_7","DOI":"10.1007\/978-3-030-03769-7_7"},{"key":"407_CR14","doi-asserted-by":"publisher","unstructured":"Havelund K, Peled D (2019) An extension of LTL with rules and its application to runtime verification, pp 239\u2013255. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-32079-9_14","DOI":"10.1007\/978-3-030-32079-9_14"},{"key":"407_CR15","doi-asserted-by":"crossref","unstructured":"Hunter G, Wei P (2019) Service-oriented separation assurance for small uas traffic management. In: INCS19, pp 1\u201311","DOI":"10.1109\/ICNSURV.2019.8735165"},{"key":"407_CR16","doi-asserted-by":"crossref","unstructured":"Kempa B, Zhang P, Jones PH, Zambreno J, Rozier KY (2020) Embedding online runtime verification for fault disambiguation on robonaut2. In FORMATS, LNCS. Springer","DOI":"10.1007\/978-3-030-57628-8_12"},{"key":"407_CR17","doi-asserted-by":"crossref","unstructured":"Li J, Vardi MY, Rozier KY (2019) Satisfiability checking for mission-time LTL. In: CAV, LNCS, vol 11562, pp 3\u201322. Springer, New York","DOI":"10.1007\/978-3-030-25543-5_1"},{"key":"407_CR18","unstructured":"Martin N (2020) FAA, NASA conclude Drone traffic mgmt pilot program\u2019s second phase; pamela whitely quoted. Online:https:\/\/www.executivegov.com\/2020\/11\/faa-nasa-conclude-drone-traffic-mgmt-pilot-programs-second-phase-pamela-whitley-quoted\/"},{"key":"407_CR19","doi-asserted-by":"crossref","unstructured":"Moosbrugger P, Rozier KY, Schumann J (2017) R2U2: Monitoring and diagnosis of security threats for unmanned aerial systems. FMSD pp 1\u201331","DOI":"10.1007\/s10703-017-0275-x"},{"key":"407_CR20","unstructured":"NASA: Unmanned Aircraft System (UAS) Traffic Management (UTM) (2020) https:\/\/utm.arc.nasa.gov\/index.shtml. Last Accessed on Mar. 12"},{"key":"407_CR21","unstructured":"NASA: Earth atmosphere model (2015) Online: https:\/\/www.grc.nasa.gov\/WWW\/K-12\/airplane\/atmosmet.html"},{"issue":"4","key":"407_CR22","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s11334-013-0223-x","volume":"9","author":"L Pike","year":"2013","unstructured":"Pike L, Wegmann N, Niller S, Goodloe A (2013) Copilot: monitoring embedded systems. Innovat Syst Softw Eng 9(4):235\u2013255","journal-title":"Innovat Syst Softw Eng"},{"key":"407_CR23","unstructured":"Reichmann K (2020) FAA, NASA UAS demonstrations mark end of UTM pilot program. Online:https:\/\/www.aviationtoday.com\/2020\/11\/18\/faa-nasa-uas-demonstrations-mark-end-utm-pilot-program\/"},{"key":"407_CR24","doi-asserted-by":"crossref","unstructured":"Reinbacher T, Rozier KY, Schumann J (2014) Temporal-logic based runtime observer pairs for system health management of real-time systems. In TACAS, pp 357\u2013372","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"407_CR25","doi-asserted-by":"crossref","unstructured":"Rios J, Mulfinger D, Homola J, Venkatesan P (2016) NASA UAS traffic management national campaign: Operations across Six UAS Test Sites. In DASC, pp 1\u20136","DOI":"10.1109\/DASC.2016.7778080"},{"key":"407_CR26","doi-asserted-by":"crossref","unstructured":"Rozier KY (2016) Specification: the biggest bottleneck in formal methods and autonomy, 9971st edn. Springer, pp 8\u201326","DOI":"10.1007\/978-3-319-48869-1_2"},{"key":"407_CR27","unstructured":"Rozier KY, Schumann J (2017) R2U2: Tool overview. RV-CUBES, 3rd edn. Kalpa Publications, Seattle, WA, USA, pp 138\u2013156"},{"key":"407_CR28","unstructured":"Rozier KY, Schumann J, Ippolito C (2015) Intelligent hardware-enabled sensor and software safety and health management for autonomous UAS. Tech. Rep. 20150021506, NASA Ames Research Center, Moffett Field, CA 94035, USA"},{"issue":"2","key":"407_CR29","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier KY, Vardi MY (2010) LTL satisfiability checking. Int J Softw Tools Technol Transfer 12(2):123\u2013137","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"407_CR30","unstructured":"Schirmer S (2016) Runtime monitoring with lola. Master\u2019s thesis, Saarland University"},{"issue":"1","key":"407_CR31","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. IJPHM 6(1):1\u201327","journal-title":"IJPHM"},{"key":"407_CR32","unstructured":"The international conference on runtime verification. Online: https:\/\/www.runtime-verification.org\/ (2001\u2013present)"},{"key":"407_CR33","doi-asserted-by":"crossref","unstructured":"Wargo CA, Glaneuski J, Hunter G, DiFelici J, Blumer T, Hasson D, Carros P, Kerczewski RJ (2018) Ubiquitous surveillance notional architecture for system-wide daa capabilities in the nas. In 2018 IEEE Aerospace Conference, pp 1\u201314","DOI":"10.1109\/AERO.2018.8396420"},{"key":"407_CR34","unstructured":"Wei P, Atkins EM, Hunter G, Rozier KY, Schnell T (2017) Pre-departure dynamic geofencing, en-route traffic alerting, emergency landing and contingency management for intelligent low-altitude airspace UAS Traffic Management. Online: https:\/\/www.nsf.gov\/awardsearch\/showAward?AWD_ID=1718420"},{"key":"407_CR35","doi-asserted-by":"crossref","unstructured":"Zhao Y, Rozier KY (2014) Formal specification and verification of a coordination protocol for an automated air traffic control system. Science of Computer Programming, P 96","DOI":"10.1016\/j.scico.2014.04.002"},{"key":"407_CR36","doi-asserted-by":"crossref","unstructured":"Zhu G, Wei P (2016) Low-altitude UAS traffic coordination with dynamic geofencing. In 16th AIAA Aviation Technology, Integration, and Operations Conference","DOI":"10.2514\/6.2016-3453"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-021-00407-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-021-00407-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-021-00407-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,14]],"date-time":"2022-11-14T09:15:13Z","timestamp":1668417313000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-021-00407-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,14]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["407"],"URL":"https:\/\/doi.org\/10.1007\/s11334-021-00407-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2021,7,14]]},"assertion":[{"value":"15 December 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 June 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 July 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}