{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T16:18:36Z","timestamp":1774369116933,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030509941","type":"print"},{"value":"9783030509958","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-50995-8_9","type":"book-chapter","created":{"date-parts":[[2020,6,19]],"date-time":"2020-06-19T23:05:25Z","timestamp":1592607925000},"page":"155-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Graphical Toolkit for the Validation of Requirements for Detect and Avoid Systems"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,20]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Carre\u00f1o, V., Consiglio, M., Mu\u00f1oz, C.: Analysis and preliminary results of a concept for detect and avoid in the cockpit. In: Proceedings of the 38th Digital Avionics Systems Conference (DASC 2019), San Diego, CA, US (September 2019)","DOI":"10.1109\/DASC43569.2019.9081766"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Chamberlain, J.P., Consiglio, M.C., Mu\u00f1oz, C.: DANTi: detect and avoid in the cockpit. In: 17th AIAA Aviation Technology, Integration, and Operations Conference, p. 4491 (2017). \nhttps:\/\/doi.org\/10.2514\/6.2017-4491","DOI":"10.2514\/6.2017-4491"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Cook, S.P., Brooks, D., Cole, R., Hackenberg, D., Raska, V.: Defining well clear for unmanned aircraft systems. In: Proceedings of the 2015 AIAA Infotech @ Aerospace Conference. No. AIAA-2015-0481, Kissimmee, Florida (January 2015). \nhttps:\/\/doi.org\/10.2514\/6.2015-0481","DOI":"10.2514\/6.2015-0481"},{"key":"9_CR4","unstructured":"Davies, J.T., Wu, M.G.: Comparative analysis of ACAS-Xu and DAIDALUS detect-and-avoid systems. Tech. rep. (2018). \nhttps:\/\/ntrs.nasa.gov\/search.jsp?R=20180001564"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-319-21215-9_6","volume-title":"Tests and Proofs","author":"AM Dutle","year":"2015","unstructured":"Dutle, A.M., Mu\u00f1oz, C.A., Narkawicz, A.J., Butler, R.W.: Software validation via model animation. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 92\u2013108. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21215-9_6"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/BFb0028775","volume-title":"Computer Aided Verification","author":"C Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR: a toolset for specifying and analyzing software requirements. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 526\u2013531. Springer, Heidelberg (1998). \nhttps:\/\/doi.org\/10.1007\/BFb0028775"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-25264-8_2","volume-title":"SDL 2011: Integrating System and Software Modeling","author":"T Le Sergent","year":"2011","unstructured":"Le Sergent, T.: SCADE: a comprehensive framework for critical system and software engineering. In: Ober, I., Ober, I. (eds.) SDL 2011. LNCS, vol. 7083, pp. 2\u20133. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-25264-8_2"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-63194-3_14","volume-title":"Software Engineering in Health Care","author":"P Masci","year":"2017","unstructured":"Masci, P., Oladimeji, P., Curzon, P., Thimbleby, H.: Using PVSio-web to demonstrate software issues in medical user interfaces. In: Huhn, M., Williams, L. (eds.) FHIES\/SEHC - 2014. LNCS, vol. 9062, pp. 214\u2013221. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63194-3_14"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-319-21690-4_30","volume-title":"Computer Aided Verification","author":"P Masci","year":"2015","unstructured":"Masci, P., Oladimeji, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H.: PVSio-web 2.0: joining PVS to HCI. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 470\u2013478. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_30"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Mu\u00f1oz, C., Narkawicz, A., Chamberlain, J., Consiglio, M., Upchurch, J.: A family of well-clear boundary models for the integration of UAS in the NAS. In: Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference. No. AIAA-2014-2412, Georgia, Atlanta, USA (June 2014). \nhttps:\/\/doi.org\/10.2514\/6.2014-2412","DOI":"10.2514\/6.2014-2412"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Mu\u00f1oz, C., Narkawicz, A., Hagen, G., Upchurch, J., Dutle, A., Consiglio, M.: DAIDALUS: detect and avoid alerting logic for unmanned systems. In: Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic (September 2015). \nhttps:\/\/doi.org\/10.1109\/DASC.2015.7311421","DOI":"10.1109\/DASC.2015.7311421"},{"key":"9_CR12","unstructured":"Narkawicz, A., Mu\u00f1oz, C., Dutle, A.: The MINERVA software development process. In: Shankar, N., Dutertre, B. (eds.) Automated Formal Methods, vol. 5, pp. 93\u2013108. Kalpa Publications in Computing. EasyChair (2018)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Narkawicz, A., Mu\u00f1oz, C., Dutle, A.: Sensor uncertainty mitigation and dynamic well clear volumes in DAIDALUS. In: Proceedings of the 37th Digital Avionics Systems Conference (DASC 2018), London, England, UK (September 2018)","DOI":"10.1109\/DASC.2018.8569468"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"9_CR15","unstructured":"RTCA SC-1228: RTCA-DO-365, Minimum Operational Performance Standards for Detect and Avoid (DAA) Systems (May 2017)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-030-13838-7_10","volume-title":"Logic-Based Program Synthesis and Transformation","author":"L Titolo","year":"2019","unstructured":"Titolo, L., Mu\u00f1oz, C.A., Feli\u00fa, M.A., Moscato, M.M.: Eliminating unstable tests in floating-point programs. In: Mesnard, F., Stuckey, P.J. (eds.) LOPSTR 2018. LNCS, vol. 11408, pp. 169\u2013183. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-13838-7_10"},{"key":"9_CR17","unstructured":"US Code of Federal Regulations: Title 14 Aeronautics and Space; Part 91 General operating and fight rules; Section 111 (1967)"},{"key":"9_CR18","unstructured":"US Code of Federal Regulations: Title 14 Aeronautics and Space; Part 91 General operating and fight rules; Section 113 (1967)"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-50995-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,19]],"date-time":"2020-06-19T23:05:46Z","timestamp":1592607946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-50995-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030509941","9783030509958"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-50995-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"20 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 June 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 June 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tap.sosy-lab.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}