{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T15:19:07Z","timestamp":1773155947928,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031937057","type":"print"},{"value":"9783031937064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-93706-4_1","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:39Z","timestamp":1749316959000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Enforcing MAVLink Safety & Security Properties via Refined Multiparty Session Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-7712-5055","authenticated-orcid":false,"given":"Arthur","family":"Amorim","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7873-9694","authenticated-orcid":false,"given":"Max","family":"Taylor","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5197-2448","authenticated-orcid":false,"given":"Trevor","family":"Kann","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3760-3556","authenticated-orcid":false,"given":"William L.","family":"Harrison","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3271-3921","authenticated-orcid":false,"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0284-4787","authenticated-orcid":false,"given":"Lance","family":"Joneckis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Allouch, A., Cheikhrouhou, O., Koub\u00e2a, A., Khalgui, M., Abbes, T.: Mavsec: securing the MAVLink protocol for ArduPilot\/PX4 unmanned aerial systems. In: 2019 15th International Wireless Communications & Mobile Computing Conference (IWCMC), pp. 621\u2013628. IEEE (2019)","DOI":"10.1109\/IWCMC.2019.8766667"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Amorim, A., Kann, T., Taylor, M., Joneckis, L.: Towards provable security in industrial control systems via dynamic protocol attestation (2024). https:\/\/arxiv.org\/abs\/2412.14467. To appear in Proceedings of the ICSS\u201924","DOI":"10.1109\/ACSACW65225.2024.00020"},{"key":"1_CR3","unstructured":"ArduPilot: Missionplanner issue #1248: Add support for new flight modes (2024). https:\/\/github.com\/ArduPilot\/MissionPlanner\/issues\/1248. Accessed 22 Nov 2024"},{"key":"1_CR4","unstructured":"ArduPilot Development Team: ArduPilot: The open source autopilot (2024). https:\/\/ardupilot.org\/. Accessed 19 Nov 2024"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.tcs.2017.02.009","volume":"669","author":"L Bocchi","year":"2017","unstructured":"Bocchi, L., Chen, T.C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33\u201358 (2017). https:\/\/doi.org\/10.1016\/j.tcs.2017.02.009","journal-title":"Theor. Comput. Sci."},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Castro-Perez, D., Ferreira, F., Gheri, L., Yoshida, N.: Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 237\u2013251. Association for Computing Machinery, New York (2021).https:\/\/doi.org\/10.1145\/3453483.3454041,","DOI":"10.1145\/3453483.3454041"},{"key":"1_CR7","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Ph.D. thesis, INRIA (1986)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.ic.2017.06.002","volume":"256","author":"O Dardha","year":"2017","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253\u2013286 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.06.002","journal-title":"Inf. Comput."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Ekici, B., Yoshida, N.: Completeness of asynchronous session tree subtyping in Coq. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0309, pp. 13:1\u201313:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2024).https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.13, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2024.13","DOI":"10.4230\/LIPIcs.ITP.2024.13"},{"issue":"2104","key":"1_CR11","doi-asserted-by":"publisher","first-page":"20150401","DOI":"10.1098\/rsta.2015.0401","volume":"375","author":"K Fisher","year":"2017","unstructured":"Fisher, K., Launchbury, J., Richards, R.: The HACMS program: using formal methods to eliminate exploitable bugs. Philos. Trans. Roy. Soc. A: Math. Phys. Eng. Sci. 375(2104), 20150401 (2017)","journal-title":"Philos. Trans. Roy. Soc. A: Math. Phys. Eng. Sci."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Hamza, M.A., Mohsin, M., Khalil, M., Kazmi, S.M.K.A.: MAVLink protocol: a survey of security threats and countermeasures. In: 2024 4th International Conference on Digital Futures and Transformative Technologies (ICoDT2), pp.\u00a01\u20138. IEEE (2024)","DOI":"10.1109\/ICoDT262145.2024.10740195"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Hickey, P.C., Pike, L., Elliott, T., Bielman, J., Launchbury, J.: Building embedded systems with embedded DSLs. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp.\u00a03\u20139 (2014)","DOI":"10.1145\/2628136.2628146"},{"key":"1_CR14","unstructured":"Honda, K.: Types for dyadic interaction* (1993). https:\/\/www.kurims.kyoto-u.ac.jp\/~kyodo\/kokyuroku\/contents\/pdf\/0851-05.pdf. Accessed 03 Sept 2024"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 273\u2013284 (2008)","DOI":"10.1145\/1328438.1328472"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Kim, H., Ozmen, M.O., Bianchi, A., Celik, Z.B., Xu, D.: PGFUZZ: policy-guided fuzzing for robotic vehicles. In: NDSS (2021)","DOI":"10.14722\/ndss.2021.24096"},{"key":"1_CR17","unstructured":"Kim, T., et al.: RVFuzzer: finding input validation bugs in robotic vehicles through Control-Guided testing. In: 28th USENIX Security Symposium (USENIX Security 19), pp. 425\u2013442. USENIX Association, Santa Clara (2019). https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/kim"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Klein, G., et\u00a0al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"43203","DOI":"10.1109\/ACCESS.2018.2863237","volume":"6","author":"YM Kwon","year":"2018","unstructured":"Kwon, Y.M., Yu, J., Cho, B.M., Eun, Y., Park, K.J.: Empirical analysis of MAVLink protocol vulnerability for attacking unmanned aerial vehicles. IEEE Access 6, 43203\u201343212 (2018)","journal-title":"IEEE Access"},{"key":"1_CR20","unstructured":"MAVLink Development Team: MAVLink: Micro air vehicle communication protocol (2024). https:\/\/mavlink.io\/. Accessed 19 Nov 2024"},{"key":"1_CR21","unstructured":"Nawrocki, W.: Towards a formalised metatheory of session types in Lean. Master\u2019s thesis, University of Glasgow (2019)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Neykova, R., Yoshida, N., Hu, R.: SPY: local verification of global protocols (2013). https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40787-1_25.pdf","DOI":"10.1007\/978-3-642-40787-1_25"},{"key":"1_CR23","unstructured":"PX4 Development Team: PX4: Open source autopilot for drones (2024). https:\/\/px4.io\/. Accessed 19 Nov 2024"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Slagel, J.T., White, L.M., Dutle, A., Mu\u00f1oz, C.A., Crespo, N.: A formal verification framework for runtime assurance. In: NASA Formal Methods Symposium, pp. 322\u2013328. Springer (2024)","DOI":"10.1007\/978-3-031-60698-4_19"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Slagel, J.T., White, L.M., Dutle, A., Mu\u00f1oz, C.A., Crespo, N.: A verification framework for runtime assurance of autonomous UAS. In: 2024 AIAA DATC\/IEEE 43rd Digital Avionics Systems Conference (DASC), pp. 01\u201308. IEEE (2024)","DOI":"10.1109\/DASC62030.2024.10748654"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Swamy, N., et\u00a0al.: Dependent types and multi-monadic effects in F. In: Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 256\u2013270 (2016)","DOI":"10.1145\/2837614.2837655"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Taylor, M., Boubin, J., Chen, H., Stewart, C., Qin, F.: A study on software bugs in unmanned aircraft systems. In: 2021 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 1439\u20131448. IEEE (2021)","DOI":"10.1109\/ICUAS51884.2021.9476844"},{"key":"1_CR28","unstructured":"Vassor, M., Yoshida, N.: Refinements for multiparty message-passing protocols: specification-agnostic theory and implementation (2024)"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: International Conference on Distributed Computing and Internet Technology, pp. 73\u201393. Springer (2019)","DOI":"10.1007\/978-3-030-36987-3_5"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Hu, R., Neykova, R., Ng, N.: The Scribble protocol language. In: Trustworthy Global Computing: 8th International Symposium, TGC 2013, Buenos Aires, Argentina, 30\u201331 August 2013, Revised Selected Papers 8, pp. 22\u201341. Springer (2014)","DOI":"10.1007\/978-3-319-05119-2_3"},{"key":"1_CR31","unstructured":"Zalakain, U.: Type-checking session-typed $$\\pi $$-calculus with Coq. Master\u2019s thesis, University of Glasgow (2019)"},{"key":"1_CR32","unstructured":"Zhou, F.: Refinement session types. Ph.D. thesis, Imperial College London (2019)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang. 4(OOPSLA), 1\u201330 (2020)","DOI":"10.1145\/3428216"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-93706-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:47Z","timestamp":1749316967000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hampton Roads, VA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}