{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:23Z","timestamp":1781193743553,"version":"3.54.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_5","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:06Z","timestamp":1781191986000},"page":"99-119","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From High-Level Types to\u00a0Low-Level Monitors: Synthesizing Verified Runtime Checkers for\u00a0MAVLink"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-7712-5055","authenticated-orcid":false,"given":"Arthur","family":"Amorim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1425-8873","authenticated-orcid":false,"given":"Paul","family":"Gazzillo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7873-9694","authenticated-orcid":false,"given":"Max","family":"Taylor","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0284-4787","authenticated-orcid":false,"given":"Lance","family":"Joneckis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"5_CR1","unstructured":"R2U2: monitoring and diagnosis of security threats for unmanned aerial systems | Formal Methods in System Design. https:\/\/link.springer.com\/article\/10.1007\/s10703-017-0275-x"},{"key":"5_CR2","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":"5_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-031-93706-4_1","volume-title":"NASA Formal Methods","author":"A Amorim","year":"2025","unstructured":"Amorim, A., Taylor, M., Kann, T., Harrison, W.L., Leavens, G.T., Joneckis, L.: Enforcing MAVLink safety & security properties via refined multiparty session types. In: Dutle, A., Humphrey, L., Titolo, L. (eds.) NASA Formal Methods. LNCS, pp. 1\u201310. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-93706-4_1"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Amorim, A., Taylor, M., Kann, T., Leavens, G.T., Harrison, W.L., Joneckis, L.: UAV resilience against stealthy attacks. In: 2025 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 994\u20131001 (2025). https:\/\/ieeexplore.ieee.org\/abstract\/document\/11007915","DOI":"10.1109\/ICUAS65942.2025.11007915"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Ancona, D., Franceschini, L., Ferrando, A., Mascardi, V.: RML: theory and practice of a domain specific language for runtime verification. Sci. Comput. Program. 205, 102610 (2021). https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642321000034","DOI":"10.1016\/j.scico.2021.102610"},{"key":"5_CR6","unstructured":"ArduPilot: MissionPlanner Issue #1248: Add support for new flight modes (2024). https:\/\/github.com\/ArduPilot\/MissionPlanner\/issues\/1248"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"CHAARI, L., CHAHBANI, S., REZGUI, J.: MAV-DTLS toward Security Enhancement of the UAV-GCS Communication. In: 2020 IEEE 92nd Vehicular Technology Conference (VTC2020-Fall), pp.\u00a01\u20135 (2020). https:\/\/ieeexplore.ieee.org\/document\/9348584, iSSN: 2577-2465","DOI":"10.1109\/VTC2020-Fall49728.2020.9348584"},{"key":"5_CR8","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":"5_CR9","doi-asserted-by":"crossref","unstructured":"Khan, S., Liew, C.F., Yairi, T., McWilliam, R.: Unsupervised anomaly detection in unmanned aerial vehicles. Appl. Soft Comput. 83, 105650 (2019). https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1568494619304302","DOI":"10.1016\/j.asoc.2019.105650"},{"key":"5_CR10","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":"5_CR11","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), Santa Clara, CA, pp. 425\u2013442. USENIX Association (2019). https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/kim"},{"key":"5_CR12","doi-asserted-by":"crossref","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). https:\/\/ieeexplore.ieee.org\/document\/8425627","DOI":"10.1109\/ACCESS.2018.2863237"},{"key":"5_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-031-98682-6_16","volume-title":"Computer Aided Verification","author":"E Li","year":"2025","unstructured":"Li, E., Stutz, F., Wies, T., Zufferey, D.: SPROUT: a verifier for symbolic multiparty protocols. In: Piskac, R., Rakamari\u0107, Z. (eds.) CAV 2025. LNCS, vol. 15933, pp. 304\u2013317. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98682-6_16"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Luckcuck, M., Ferrando, A., Faruq, F.: Varanus: runtime Verification for CSP. In: Cavalcanti, A., Foster, S., Richardson, R. (eds.) TAROS 2025. LNCS, vol. 16045, pp. 259\u2013272. Springer, Heidelberg (2025). https:\/\/doi.org\/10.1007\/978-3-032-01486-3_21","DOI":"10.1007\/978-3-032-01486-3_21"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-030-17184-1_2","volume-title":"Programming Languages and Systems","author":"G Mart\u00ednez","year":"2019","unstructured":"Mart\u00ednez, G., et al.: Meta-F$$^\\star $$: proof automation with SMT, tactics, and metaprograms. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 30\u201359. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_2"},{"key":"5_CR16","unstructured":"MAVLink Development Team: MAVLink: Micro Air Vehicle Communication Protocol (2024). https:\/\/mavlink.io\/"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Protzenko, J., et al.: Verified low-level programming embedded in F. Proc. ACM Program. Lang. 1(ICFP), 1\u201329 (2017)","DOI":"10.1145\/3110261"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Swamy, N., et al.: 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":"5_CR20","doi-asserted-by":"crossref","unstructured":"Taylor, M., Amorim, A., Joneckis, L.: Securing Modbus-based industrial control systems with refined multiparty session types. In: 2025 Annual Computer Security Applications Conference Workshops (ACSAC Workshops), pp. 99\u2013109 (2025). https:\/\/ieeexplore.ieee.org\/abstract\/document\/11418027","DOI":"10.1109\/ACSACW69556.2025.00016"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Taylor, M., Chen, H., Qin, F., Stewart, C.: Avis: in-situ model checking for unmanned aerial vehicles. In: 2021 51st Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 471\u2013483. IEEE (2021)","DOI":"10.1109\/DSN48987.2021.00057"},{"key":"5_CR22","unstructured":"Vassor, M., Yoshida, N.: Refinements for multiparty message-passing protocols: specification-agnostic theory and implementation. In: Aldrich, J., Salvaneschi, G. (eds.) 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0313, pp. 41:1\u201341:29. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ECOOP.2024.41"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Wray, T., Wang, Y.: PAVE-MAVLink: formal verification of MAVLink 2 for secure UAV communications. In: MILCOM 2025 - 2025 IEEE Military Communications Conference (MILCOM), pp. 1389\u20131395 (2025). https:\/\/ieeexplore.ieee.org\/document\/11310743","DOI":"10.1109\/MILCOM64451.2025.11310743"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-05119-2_3","volume-title":"Trustworthy Global Computing","author":"N Yoshida","year":"2014","unstructured":"Yoshida, N., Hu, R., Neykova, R., Ng, N.: The scribble protocol language. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 22\u201341. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-05119-2_3"},{"key":"5_CR25","unstructured":"Zhou, F.: Refining Multiparty Session Types. Ph.D. thesis, Imperial College London, London, UK (2024). https:\/\/doi.org\/10.25560\/110416"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. In: Proceedings of the ACM on Programming Languages, vol. 4no. OOPSLA, pp. 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-032-28079-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:16Z","timestamp":1781191996000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","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":"Los Angeles, CA","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}