{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T17:49:28Z","timestamp":1777657768856,"version":"3.51.4"},"publisher-location":"Cham","reference-count":51,"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_3","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:23:02Z","timestamp":1749316982000},"page":"31-53","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards a\u00a0Safe, Verified Runtime Monitor for\u00a0Embedded Systems: R2U2 in\u00a0Embedded Rust"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2008-673X","authenticated-orcid":false,"given":"Alexis","family":"Aurandt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8220-7552","authenticated-orcid":false,"given":"Phillip H.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"3_CR1","unstructured":"A no_std rust environment. https:\/\/docs.rust-embedded.org\/book\/intro\/no-std.html"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. In: LICS, pp. 390\u2013401. IEEE (1990)","DOI":"10.1109\/LICS.1990.113764"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., et al.: The prusti project: Formal verification for rust. In: NASA Formal Methods Symposium, pp. 88\u2013108. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_5","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3(OOPSLA), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3360573","DOI":"10.1145\/3360573"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Aurandt, A., Jones, P.H., Rozier, K.Y.: Runtime verification triggers real-time, autonomous fault recovery on the cysat-i. In: NASA Formal Methods Symposium, pp. 816\u2013825. Springer, Cham (2022). https:\/\/temporallogic.org\/research\/CySat-NFM22\/CySat-NFM22.pdf","DOI":"10.1007\/978-3-031-06773-0_45"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Aurandt, A., Jones, P.H., Rozier, K.Y., Wongpiromsarn, T.: Multimodal model predictive runtime verification for safety of autonomous cyber-physical systems. In: International Conference on Formal Methods for Industrial Critical Systems. pp. 220\u2013244. Springer, Cham (2024). https:\/\/temporallogic.org\/research\/MMPRV\/MMPRV.pdf","DOI":"10.1007\/978-3-031-68150-9_13"},{"key":"3_CR7","unstructured":"Barrett, C., Stump, A., Tinelli, C., et\u00a0al.: The smt-lib standard: version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), vol.\u00a013, p.\u00a014 (2010)"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. Lectures on Runtime Verification: Introductory and Advanced Topics, pp. 135\u2013175 (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Basin, D., et\u00a0al.: Verimon: a formally verified monitoring tool. In: International Colloquium on Theoretical Aspects of Computing, pp.\u00a01\u20136. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_1","DOI":"10.1007\/978-3-031-17715-6_1"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-030-51074-9_25","volume-title":"Automated Reasoning","author":"D Basin","year":"2020","unstructured":"Basin, D., et al.: A formally verified, optimized monitor for metric first-order dynamic logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 432\u2013453. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_25"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Finkbeiner, B., Kohn, F., Scheerer, F.: A tutorial on stream-based monitoring. In: International Symposium on Formal Methods, pp. 624\u2013648. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_33","DOI":"10.1007\/978-3-031-71177-0_33"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/978-3-642-34281-3_34","volume-title":"Formal Methods and Software Engineering","author":"JO Blech","year":"2012","unstructured":"Blech, J.O., Falcone, Y., Becker, K.: Towards certified runtime verification. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 494\u2013509. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34281-3_34"},{"key":"3_CR13","unstructured":"Cauwels, M., Hammer, A., Hertz, B., Jones, P., Rozier, K.Y.: Integrating runtime verification into an automated UAS traffic management system. In: DETECT. Springer, L\u2019Aquila, Italy (2020). https:\/\/r2u2.temporallogic.org\/wp-content\/uploads\/2020\/12\/CHHJR20.pdf"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-030-60508-7_21","volume-title":"Runtime Verification","author":"A Chattopadhyay","year":"2020","unstructured":"Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 383\u2013403. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_21"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Dabney, J.B., Badger, J.M., Rajagopal, P.: Trustworthy autonomy for gateway vehicle system manager. In: 2023 IEEE Space Computing Conference (SCC), pp. 57\u201362. IEEE (2023). https:\/\/doi.org\/10.1109\/SCC57168.2023.00018","DOI":"10.1109\/SCC57168.2023.00018"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Denis, X., Jourdan, J.H., March\u00e9, C.: Creusot: a foundry for the deductive verification of rust programs. In: International Conference on Formal Engineering Methods, pp. 90\u2013105. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_6","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Durumeric, Z., et\u00a0al.: The matter of heartbleed. In: Proceedings of the 2014 Conference on Internet Measurement Conference, pp. 475\u2013488 (2014). https:\/\/doi.org\/10.1145\/2663716.2663755","DOI":"10.1145\/2663716.2663755"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Efficient temporal logic runtime monitoring for tiny systems. In: International Conference on Tests and Proofs, pp. 3\u201321. Springer, Cham (2024). https:\/\/www.ruediger-ehlers.de\/papers\/tap2024.pdf","DOI":"10.1007\/978-3-031-72044-4_1"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-030-60508-7_24","volume-title":"Runtime Verification","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Oswald, S., Passing, N., Schwenger, M.: Verified rust monitors for lola specifications. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 431\u2013450. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_24"},{"issue":"1","key":"3_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10458-020-09487-2","volume":"35","author":"M Fisher","year":"2020","unstructured":"Fisher, M., Mascardi, V., Rozier, K.Y., Schlingloff, B.-H., Winikoff, M., Yorke-Smith, N.: Towards a framework for certification of reliable autonomous systems. Auton. Agent. Multi-Agent Syst. 35(1), 1\u201365 (2020). https:\/\/doi.org\/10.1007\/s10458-020-09487-2","journal-title":"Auton. Agent. Multi-Agent Syst."},{"issue":"4","key":"3_CR23","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/MC.2023.3322902","volume":"57","author":"AE Goodloe","year":"2024","unstructured":"Goodloe, A.E., Havelund, K.: High-integrity runtime verification. Computer 57(4), 37\u201345 (2024). https:\/\/doi.org\/10.1109\/MC.2023.3322902","journal-title":"Computer"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-76384-8_10","volume-title":"NASA Formal Methods","author":"B Hertz","year":"2021","unstructured":"Hertz, B., Luppen, Z., Rozier, K.Y.: Integrating runtime verification into a sounding rocket control system. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 151\u2013159. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_10"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Johannsen, C., et\u00a0al.: Openuas version 1.0. In: 2021 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 1449\u20131458. IEEE (2021). https:\/\/doi.org\/10.1109\/ICUAS51884.2021.9476814","DOI":"10.1109\/ICUAS51884.2021.9476814"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Johannsen, C., Jones, P., Kempa, B., Rozier, K.Y., Zhang, P.: R2u2 version 3.0: re-imagining a toolchain for specification, resource estimation, and optimized observer generation for runtime verification in hardware and software. In: International Conference on Computer Aided Verification, pp. 483\u2013497. Springer (2023). https:\/\/research.temporallogic.org\/papers\/JJKRZ23.pdf","DOI":"10.1007\/978-3-031-37709-9_23"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Johannsen, C., Kempa, B., Jones, P.H., Rozier, K.Y., Wongpiromsarn, T.: Impossible made possible: Encoding intractable specifications via implied domain constraints. In: International Conference on Formal Methods for Industrial Critical Systems, pp. 151\u2013169. Springer, Cham (2023). https:\/\/research.temporallogic.org\/papers\/JKJRW23.pdf","DOI":"10.1007\/978-3-031-43681-9_9"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Kallwies, H., Leucker, M., Schmitz, M., Schulz, A., Thoma, D., Weiss, A.: Tessla\u2013an ecosystem for runtime verification. In: International Conference on Runtime Verification, pp. 314\u2013324. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_20","DOI":"10.1007\/978-3-031-17196-3_20"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y.: Embedding online runtime verification for fault disambiguation on Robonaut2. In: Proceedings of the 18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 196\u2013214. Lecture Notes in Computer Science (LNCS), Springer, Vienna (2020). http:\/\/research.temporallogic.org\/papers\/KZJZR20.pdf","DOI":"10.1007\/978-3-030-57628-8_12"},{"key":"3_CR30","unstructured":"Kempa, B.C.S.: Enumerating test cases for mltl runtime monitors. In: Engineering trust in space with runtime verification. Ph.D. thesis. Iowa State University (2024)"},{"key":"3_CR31","unstructured":"Kosaian, K., Wang, Z., Sloan, E., Rozier, K.: Formalizing MLTL formula progression in isabelle\/hol. arXiv preprint arXiv:2410.03465 (2024). https:\/\/arxiv.org\/abs\/2410.03465"},{"issue":"4","key":"3_CR32","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-time Syst. 2(4), 255\u2013299 (1990). https:\/\/doi.org\/10.1007\/BF01995674","journal-title":"Real-time Syst."},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Lattuada, A., et\u00a0al.: Verus: a practical foundation for systems verification. In: Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, pp. 438\u2013454 (2024). https:\/\/doi.org\/10.1145\/3694715.3695952","DOI":"10.1145\/3694715.3695952"},{"issue":"OOPSLA1","key":"3_CR34","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1145\/3586037","volume":"7","author":"A Lattuada","year":"2023","unstructured":"Lattuada, A., et al.: Verus: verifying rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA1), 286\u2013315 (2023). https:\/\/doi.org\/10.1145\/3586037","journal-title":"Proc. ACM Program. Lang."},{"issue":"7","key":"3_CR35","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"NG Leveson","year":"1993","unstructured":"Leveson, N.G., Turner, C.S.: An investigation of the therac-25 accidents. Computer 26(7), 18\u201341 (1993). https:\/\/doi.org\/10.1109\/MC.1993.274940","journal-title":"Computer"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-25543-5_1","volume-title":"Computer Aided Verification","author":"J Li","year":"2019","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 3\u201322. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_1"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Pinho, A., Couto, L., Oliveira, J.: Towards rust for critical systems. In: 2019 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 19\u201324. IEEE (2019). https:\/\/doi.org\/10.1109\/ISSREW.2019.00036","DOI":"10.1109\/ISSREW.2019.00036"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-030-59152-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"M Raszyk","year":"2020","unstructured":"Raszyk, M., Basin, D., Traytel, D.: Multi-head monitoring of metric dynamic logic. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 233\u2013250. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_13"},{"key":"3_CR41","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10703-013-0199-z","volume":"44","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., F\u00fcgger, M., Brauer, J.: Runtime verification of embedded real-time systems. Formal Methods Syst. Des. 44, 203\u2013239 (2014). https:\/\/doi.org\/10.1007\/s10703-013-0199-z","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357\u2013372. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24"},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-030-32079-9_18","volume-title":"Runtime Verification","author":"J Schneider","year":"2019","unstructured":"Schneider, J., Basin, D., Krsti\u0107, S., Traytel, D.: A formally verified monitor for metric first-order temporal logic. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 310\u2013328. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_18"},{"key":"3_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-319-23820-3_15","volume-title":"Runtime Verification","author":"J Schumann","year":"2015","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 233\u2013249. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_15"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Schumann, J., Rozier, K.Y., Reinbacher, T., Mengshoel, O.J., Mbaya, T., Ippolito, C.: Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. In: PHM, pp. 381\u2013401 (2013). https:\/\/research.temporallogic.org\/papers\/SRRMMI15.pdf","DOI":"10.36001\/phmconf.2013.v5i1.2275"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Scott, R.G., Dodds, M., Perez, I., Goodloe, A.E., Dockins, R.: Trustworthy runtime verification via bisimulation (experience report). Proc. ACM Program. Lang. 7(ICFP), 305\u2013321 (2023). https:\/\/doi.org\/10.1145\/3607841","DOI":"10.1145\/3607841"},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Seidel, L., Beier, J.: Bringing rust to safety-critical systems in space. In: 2024 Security for Space Systems (3S), pp.\u00a01\u20138. IEEE (2024). https:\/\/doi.org\/10.23919\/3S60530.2024.10592287","DOI":"10.23919\/3S60530.2024.10592287"},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Sharma, A., Sharma, S., Tanksalkar, S.R., Torres-Arias, S., Machiry, A.: Rust for embedded systems: current state and open problems. In: Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, pp. 2296\u20132310 (2024). https:\/\/doi.org\/10.1145\/3658644.3690275","DOI":"10.1145\/3658644.3690275"},{"key":"3_CR49","unstructured":"STMicroelectronics: Discovery kit with STM32F303VC MCU. https:\/\/www.st.com\/resource\/en\/user_manual\/um1570-discovery-kit-with-stm32f303vc-mcu-stmicroelectronics.pdf"},{"key":"3_CR50","unstructured":"Weston, D.: Windows security best practices for integrating and managing security tools (2024). https:\/\/www.microsoft.com\/en-us\/security\/blog\/2024\/07\/27\/windows-security-best-practices-for-integrating-and-managing-security-tools\/"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Zhang, P., Aurandt, A., Dureja, R., Jones, P.H., Rozier, K.Y.: Model predictive runtime verification for cyber-physical systems with real-time deadlines. In: International Conference on Formal Modeling and Analysis of Timed Systems, pp. 158\u2013180. Springer, Cham (2023). https:\/\/research.temporallogic.org\/papers\/ZADJR23.pdf","DOI":"10.1007\/978-3-031-42626-1_10"}],"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_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:23:06Z","timestamp":1749316986000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_3","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"}}]}}