{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T16:34:22Z","timestamp":1782405262067,"version":"3.54.5"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,8,8]],"date-time":"2016-08-08T00:00:00Z","timestamp":1470614400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2016,8,8]]},"abstract":"<jats:p>As the technological and operational capabilities of unmanned aircraft systems (UAS) have grown, so too have international efforts to integrate UAS into civil airspace. However, one of the major concerns that must be addressed in realizing this integration is that of safety. For example, UAS lack an on-board pilot to comply with the legal requirement that pilots see and avoid other aircraft. This requirement has motivated the development of a detect and avoid (DAA) capability for UAS that provides situational awareness and maneuver guidance to UAS operators to aid them in avoiding and remaining well clear of other aircraft in the airspace. The NASA Langley Research Center Formal Methods group has played a fundamental role in the development of this capability. This article gives a selected survey of the formal methods work conducted in support of the development of a DAA concept for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations.<\/jats:p>","DOI":"10.1145\/2984450.2984459","type":"journal-article","created":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T02:50:29Z","timestamp":1585968629000},"page":"67-76","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Unmanned aircraft systems in the national airspace system"],"prefix":"10.1145","volume":"3","author":[{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"first","affiliation":[{"name":"NASA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Dutle","sequence":"additional","affiliation":[{"name":"NASA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anthony","family":"Narkawicz","sequence":"additional","affiliation":[{"name":"NASA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jason","family":"Upchurch","sequence":"additional","affiliation":[{"name":"NASA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,8,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 31st IEEE\/AIAA Digital Avionics Systems Conference (DASC). 8A4-1--8A4-10","author":"Adaska Jason","year":"2012"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of 28th International Congress of the Aeronautical Sciences, ICAS 2012","author":"Consiglio Mar\u00eda","year":"2012"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2015-0481"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2009-1926"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2007-6611"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_14"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21215-9_6"},{"key":"e_1_2_1_8_1","volume-title":"Sponsored Sense and Avoid Workshop. 2009","author":"FAA","year":"2009"},{"key":"e_1_2_1_9_1","first-page":"566","article-title":"Horizontal miss distance filter system for suppressing false resolution alerts. (October 1996)","volume":"5","author":"Hammer Jonathan","year":"1996","journal-title":"U.S. Patent"},{"key":"e_1_2_1_10_1","unstructured":"International Civil Aviation Organization (ICAO). 2005a. Annex 2 to the Convention on International Civil Aviation. (July 2005).  International Civil Aviation Organization (ICAO). 2005a. Annex 2 to the Convention on International Civil Aviation. (July 2005)."},{"key":"e_1_2_1_11_1","unstructured":"International Civil Aviation Organization (ICAO). 2005b. Annex 2 to the Convention on International Civil Aviation. (July 2005).  International Civil Aviation Organization (ICAO). 2005b. Annex 2 to the Convention on International Civil Aviation. (July 2005)."},{"key":"e_1_2_1_12_1","unstructured":"Darryl Jenkins and Bijan Vasigh. 2013. The economic impact of Unmanned Aircraft Systems integration in the United States. Economic report of the Association For Unmanned Vehicle Systems International (AUVSI). (March 2013).  Darryl Jenkins and Bijan Vasigh. 2013. The economic impact of Unmanned Aircraft Systems integration in the United States. Economic report of the Association For Unmanned Vehicle Systems International (AUVSI). (March 2013)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_20"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9256-3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2013-4622"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2014-2412"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 34th Digital Avionics Systems Conference (DASC","author":"Mu\u00f1oz C\u00e9sar","year":"2015"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_17"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9320-x"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/648230.752639"},{"key":"e_1_2_1_22_1","unstructured":"RTCA SC-147. 2009. RTCA-DO-185B Minimum operational performance standards for traffic alert and collision avoidance system II (TCAS II). (July 2009).  RTCA SC-147. 2009. RTCA-DO-185B Minimum operational performance standards for traffic alert and collision avoidance system II (TCAS II). (July 2009)."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNSurv.2014.6819987"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2011 Tyrrhenian International Workshop on Digital Communications-Enhanced Surveillance of Aircraft and Vehicles (TIWDC\/ESAV). IEEE","author":"Tomasello Filippo","year":"2011"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.2514\/atcq.23.4.275"},{"key":"e_1_2_1_26_1","unstructured":"US Code of Federal Regulations. 1967a. Title 14 Aeronautics and Space; Part 91 General operating and fight rules. (1967).  US Code of Federal Regulations. 1967a. Title 14 Aeronautics and Space; Part 91 General operating and fight rules. (1967)."},{"key":"e_1_2_1_27_1","unstructured":"US Code of Federal Regulations. 1967b. Title 14 Aeronautics and Space; Part 91 General operating and fight rules. (1967).  US Code of Federal Regulations. 1967b. Title 14 Aeronautics and Space; Part 91 General operating and fight rules. (1967)."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2011-6921"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2984450.2984459","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2984450.2984459","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:39:46Z","timestamp":1750217986000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2984450.2984459"}},"subtitle":["a formal methods perspective"],"short-title":[],"issued":{"date-parts":[[2016,8,8]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,8,8]]}},"alternative-id":["10.1145\/2984450.2984459"],"URL":"https:\/\/doi.org\/10.1145\/2984450.2984459","relation":{},"ISSN":["2372-3491"],"issn-type":[{"value":"2372-3491","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,8,8]]},"assertion":[{"value":"2016-08-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}