{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:04:29Z","timestamp":1781193869615,"version":"3.54.1"},"publisher-location":"Cham","reference-count":68,"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_4","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:59Z","timestamp":1781191979000},"page":"73-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From Natural Language Requirements to\u00a0Runtime Monitors for Resource-Constrained Systems: Integrating FRET and\u00a0R2U2"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2008-673X","authenticated-orcid":false,"given":"Alexis","family":"Aurandt","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7671-2720","authenticated-orcid":false,"given":"Christopher","family":"Johannsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7013-1100","authenticated-orcid":false,"given":"Andreas","family":"Katis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8220-7552","authenticated-orcid":false,"given":"Phillip H.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","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 (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_45","DOI":"10.1007\/978-3-031-06773-0_45"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Aurandt, A., Jones, P.H., Rozier, K.Y.: Towards a safe, verified runtime monitor for embedded systems: R2U2 in embedded rust. In: NASA Formal Methods Symposium, pp. 31\u201353. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-93706-4_3","DOI":"10.1007\/978-3-031-93706-4_3"},{"key":"4_CR3","doi-asserted-by":"publisher","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 (2024). https:\/\/doi.org\/10.1007\/978-3-031-68150-9_13","DOI":"10.1007\/978-3-031-68150-9_13"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Aurandt, A., Rozier, K.Y., Jones, P.H.: R2U2 playground: visualization of a real-time, temporal logic runtime monitor. In: Formal Methods in Computer Aided Design, pp. 126\u2013132. TU Wien Academic Press (2025). https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_18","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_18"},{"issue":"7","key":"4_CR5","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1109\/TSE.2015.2398877","volume":"41","author":"M Autili","year":"2015","unstructured":"Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., Tang, A.: Aligning qualitative, real-time, and probabilistic property specification patterns using a structured english grammar. IEEE Trans. Software Eng. 41(7), 620\u2013638 (2015). https:\/\/doi.org\/10.1109\/TSE.2015.2398877","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 415\u2013442. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"4_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":"4_CR8","doi-asserted-by":"publisher","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: 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":"4_CR9","doi-asserted-by":"publisher","unstructured":"Bauer, A., Leucker, M.: The theory and practice of SALT. In: NASA Formal Methods Symposium, pp. 13\u201340. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_3","DOI":"10.1007\/978-3-642-20398-5_3"},{"key":"4_CR10","unstructured":"Becker, S., et al.: Hanfor: semantic requirements review at scale. In: REFSQ Workshops, vol.\u00a02857, p.\u00a05 (2021)"},{"key":"4_CR11","unstructured":"Bozzano, M., et al.: nuXmv 2.1.0 user manual. Fondazione Bruno Kessler, Technical Report, Trento, Italy (2024)"},{"key":"4_CR12","doi-asserted-by":"publisher","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 (2020). https:\/\/doi.org\/10.1007\/978-3-030-59155-7_26","DOI":"10.1007\/978-3-030-59155-7_26"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: International Conference on Computer Aided Verification, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Conrad, E., Titolo, L., Giannakopoulou, D., Pressburger, T., Dutle, A.: A compositional proof framework for FRETish requirements. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 68\u201381 (2022). https:\/\/doi.org\/10.1145\/3497775.3503685","DOI":"10.1145\/3497775.3503685"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Crapo, A., Moitra, A., McMillan, C., Russell, D.: Requirements capture and analysis in ASSERT (TM). In: 2017 IEEE 25th International Requirements Engineering Conference (RE), pp. 283\u2013291. IEEE (2017). https:\/\/doi.org\/10.1109\/RE.2017.54","DOI":"10.1109\/RE.2017.54"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Dabney, J.B., Badger, J.M., Rajagopal, P.: Adding a verification view for an autonomous real-time system architecture. In: Proceedings of SciTech Forum. p. Online. 2021-0566. AIAA (2021). https:\/\/doi.org\/10.2514\/6.2021-0566","DOI":"10.2514\/6.2021-0566"},{"key":"4_CR17","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":"4_CR18","unstructured":"Dabney, J.B.: Using assume-guarantee contracts in autonomous spacecraft. Flight Software Workshop (FSW) (2021). https:\/\/www.youtube.com\/watch?v=zrtyiyNf674"},{"key":"4_CR19","unstructured":"Dabney, J.B., Rajagopal, P., Badger, J.M.: Using assume-guarantee contracts for developmental verification of autonomous spacecraft. Flight Software Workshop (FSW) (2022). https:\/\/www.youtube.com\/watch?v=HFnn6TzblPg"},{"key":"4_CR20","unstructured":"Duffy, D.A.: Principles of Automated Theorem Proving. Wiley (1991)"},{"key":"4_CR21","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 (2024). https:\/\/www.ruediger-ehlers.de\/papers\/tap2024.pdf","DOI":"10.1007\/978-3-031-72044-4_1"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Elwing, J., Gamboa-Guzman, L., Sorkin, J., Travesset, C., Wang, Z., Rozier, K.Y.: Mission-time LTL (MLTL) formula validation via regular expressions. In: International Conference on Integrated Formal Methods, pp. 279\u2013301. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_15","DOI":"10.1007\/978-3-031-47705-8_15"},{"key":"4_CR23","unstructured":"Ferreira, R.R.: Runtime verification of low-level software in a VTOL UAV (2025). https:\/\/repositorio.ufsc.br\/xmlui\/bitstream\/handle\/123456789\/263713\/Runtime_Verification_of_Low-Level_Software_in_a_VTOL_UAV.pdf"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Fifarek, A.W., Wagner, L.G., Hoffman, J.A., Rodes, B.D., Aiello, M.A., Davis, J.A.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: NASA Formal Methods Symposium, pp. 420\u2013426. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_30","DOI":"10.1007\/978-3-319-57288-8_30"},{"key":"4_CR25","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10458-020-09487-2"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and Bayesian network reasoners on-board FPGAs: flight-certifiable system health management for embedded systems. In: International Conference on Runtime Verification, pp. 215\u2013230. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_18","DOI":"10.1007\/978-3-319-11164-3_18"},{"key":"4_CR27","unstructured":"Giannakopoulou, D., Mavridou, A., Rhein, J., Pressburger, T., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020) (2020)"},{"key":"4_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106590","volume":"137","author":"D Giannakopoulou","year":"2021","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Automated formalization of structured natural language requirements. Inf. Softw. Technol. 137, 106590 (2021). https:\/\/doi.org\/10.1016\/j.infsof.2021.106590","journal-title":"Inf. Softw. Technol."},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Goodloe, A.: Challenges in high-assurance runtime verification. In: International Symposium on Leveraging Applications of Formal Methods, pp. 446\u2013460. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_31","DOI":"10.1007\/978-3-319-47166-2_31"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Greenman, B., Saarinen, S., Nelson, T., Krishnamurthi, S.: Little tricky logic: misconceptions in the understanding of LTL. arXiv preprint arXiv:2211.01677 (2022)","DOI":"10.22152\/programming-journal.org\/2023\/7\/7"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Hariharan, G., Jones, P.H., Rozier, K.Y., Wongpiromsarn, T.: Maximum satisfiability of mission-time linear temporal logic. In: International Conference on Formal Modeling and Analysis of Timed Systems, pp. 86\u2013104. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_6","DOI":"10.1007\/978-3-031-42626-1_6"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Hertz, B., Luppen, Z., Rozier, K.Y.: Integrating runtime verification into a sounding rocket control system. In: NASA Formal Methods Symposium, pp. 151\u2013159. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_10","DOI":"10.1007\/978-3-030-76384-8_10"},{"key":"4_CR33","unstructured":"Jeannet, B., Gaucher, F.: Debugging embedded systems requirements with STIMULUS: an automotive case-study. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016) (2016)"},{"key":"4_CR34","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":"4_CR35","doi-asserted-by":"publisher","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:\/\/doi.org\/10.1007\/978-3-031-37709-9_23","DOI":"10.1007\/978-3-031-37709-9_23"},{"key":"4_CR36","doi-asserted-by":"publisher","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 (2023). https:\/\/doi.org\/10.1007\/978-3-031-43681-9_9","DOI":"10.1007\/978-3-031-43681-9_9"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Johannsen, C., Jones, P.H., Rozier, K.Y., Wongpiromsarn, T.: Scalable MLTL runtime monitoring and satisfiability via bit-vector encoding. In: Formal Methods in Computer-Aided Design (FMCAD). TU Wien Academic Press (2025). https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_9","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_9"},{"key":"4_CR38","unstructured":"Johannsen, C.G.: Dynamic set reasoning: specifying and optimizing monitor encodings. Master\u2019s thesis, Iowa State University (2024)"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Katis, A., Mavridou, A., Giannakopoulou, D., Pressburger, T., Schumann, J.: Capture, analyze, diagnose: realizability checking of requirements in FRET. In: International Conference on Computer Aided Verification, pp. 490\u2013504. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_24","DOI":"10.1007\/978-3-031-13188-2_24"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Katis, A., Mavridou, A., Pressburger, T.: A streamlined, formal approach to requirements-based testing. In: NASA Formal Methods Symposium, pp. 159\u2013179. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-93706-4_10","DOI":"10.1007\/978-3-031-93706-4_10"},{"key":"4_CR41","doi-asserted-by":"publisher","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 (2020). https:\/\/doi.org\/10.1007\/978-3-030-57628-8_12","DOI":"10.1007\/978-3-030-57628-8_12"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Konrad, S., Cheng, B.H.: Automated analysis of natural language properties for UML models. In: International Conference on Model Driven Engineering Languages and Systems, pp. 48\u201357. Springer (2005). https:\/\/doi.org\/10.1007\/11663430_6","DOI":"10.1007\/11663430_6"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: International Conference on Computer Aided Verification, pp. 3\u201322. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_1","DOI":"10.1007\/978-3-030-25543-5_1"},{"key":"4_CR44","doi-asserted-by":"publisher","unstructured":"Li, R., Gurushankar, K., Heule, M.J., Rozier, K.Y.: What\u2019s in a name? Linear temporal logic literally represents time lines. In: 2023 IEEE Working Conference on Software Visualization (VISSOFT), pp. 73\u201383. IEEE (2023). https:\/\/doi.org\/10.1109\/VISSOFT60811.2023.00018","DOI":"10.1109\/VISSOFT60811.2023.00018"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Lorch, R., et al.: Formal methods in requirements engineering: survey and future directions. In: Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 88\u201399 (2024). https:\/\/doi.org\/10.1145\/3644033.3644373","DOI":"10.1145\/3644033.3644373"},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Luppen, Z., et al.: Elucidation and analysis of specification patterns in aerospace system telemetry. In: NASA Formal Methods Symposium, pp. 527\u2013537. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_28","DOI":"10.1007\/978-3-031-06773-0_28"},{"key":"4_CR47","doi-asserted-by":"publisher","unstructured":"Luppen, Z.A., Lee, D.Y., Rozier, K.Y.: A case study in formal specification and runtime verification of a cubesat communications system. In: AIAA Scitech 2021 Forum (2021). https:\/\/doi.org\/10.2514\/6.2021-0997","DOI":"10.2514\/6.2021-0997"},{"key":"4_CR48","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Katis, A., Giannakopoulou, D., Kooi, D., Pressburger, T., Whalen, M.W.: From partial to global assume-guarantee contracts: compositional realizability analysis in FRET. In: International Symposium on Formal Methods, pp. 503\u2013523. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_27","DOI":"10.1007\/978-3-030-90870-6_27"},{"key":"4_CR49","unstructured":"Mavridou, A., Katis, A., Schumann, J., Pressburger, T., Flores, G.V.: FRET: 3.0 (2025), GitHub release. https:\/\/github.com\/NASA-SW-VnV\/fret\/releases\/tag\/v3.0.0"},{"key":"4_CR50","doi-asserted-by":"publisher","unstructured":"Nayak, A., Timmapathini, H.P., Murali, V., Ponnalagu, K., Venkoparao, V.G., Post, A.: Req2Spec: transforming software requirements into formal specifications using natural language processing. In: International Working Conference on Requirements Engineering: Foundation for Software Quality, pp. 87\u201395. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-98464-9_8","DOI":"10.1007\/978-3-030-98464-9_8"},{"key":"4_CR51","doi-asserted-by":"publisher","unstructured":"Perez, I., Mavridou, A., Pressburger, T., Goodloe, A., Giannakopoulou, D.: Automated translation of natural language requirements to runtime monitors. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 387\u2013395. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_21","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"4_CR52","doi-asserted-by":"publisher","unstructured":"Prasad, S., Greenman, B., Nelson, T., Krishnamurthi, S.: A misconception-driven adaptive tutor for linear temporal logic. In: International Conference on Computer Aided Verification, pp. 185\u2013200. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_9","DOI":"10.1007\/978-3-031-98685-7_9"},{"key":"4_CR53","doi-asserted-by":"crossref","unstructured":"Pressburger, T., Katis, A., Dutle, A., Mavridou, A.: Using fret to create, analyze and monitor requirements for a lift plus cruise case study. Technical report TM-20220017032, NASA (2023)","DOI":"10.1007\/978-3-031-29786-1_21"},{"key":"4_CR54","doi-asserted-by":"publisher","unstructured":"Pressburger, T., Katis, A., Dutle, A., Mavridou, A.: Authoring, analyzing, and monitoring requirements for a lift-plus-cruise aircraft. In: International Working Conference on Requirements Engineering: Foundation for Software Quality, pp. 295\u2013308. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-29786-1_21","DOI":"10.1007\/978-3-031-29786-1_21"},{"key":"4_CR55","doi-asserted-by":"publisher","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science (LNCS), vol.\u00a08413, pp. 357\u2013372. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"4_CR56","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Verified Software. Theories, Tools, and Experiments: 8th International Conference, VSTTE 2016, Toronto, ON, Canada, 17\u201318 July 2016, pp. 8\u201326. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2","DOI":"10.1007\/978-3-319-48869-1_2"},{"key":"4_CR57","doi-asserted-by":"crossref","unstructured":"Rozier, K.Y., Schumann, J.: R2U2: tool overview. In: Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES), vol.\u00a03, pp. 138\u2013156. Kalpa Publications, Seattle, WA, USA (2017). https:\/\/easychair.org\/publications\/paper\/Vncw","DOI":"10.29007\/5pch"},{"key":"4_CR58","doi-asserted-by":"publisher","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Runtime Verification: 6th International Conference, RV 2015, Vienna, Austria, 22\u201325 September 2015, Proceedings, pp. 233\u2013249. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_15","DOI":"10.1007\/978-3-319-23820-3_15"},{"key":"4_CR59","doi-asserted-by":"publisher","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: a tool exhibition report. In: Proceedings of the 16th International Conference on Runtime Verification (RV16). Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_35","DOI":"10.1007\/978-3-319-46982-9_35"},{"key":"4_CR60","doi-asserted-by":"publisher","unstructured":"Schumann, J., Roychoudhury, I., Kulkarni, C.: Diagnostic reasoning using prognostic information for unmanned aerial systems. In: Annual Conference of the PHM Society, vol. 7 (2015). https:\/\/doi.org\/10.36001\/phmconf.2015.v7i1.2548","DOI":"10.36001\/phmconf.2015.v7i1.2548"},{"key":"4_CR61","doi-asserted-by":"publisher","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. Int. J. Prognostics Health Manag. (2015). https:\/\/doi.org\/10.36001\/ijphm.2015.v6i1.2243","DOI":"10.36001\/ijphm.2015.v6i1.2243"},{"key":"4_CR62","doi-asserted-by":"publisher","unstructured":"Sljivo, I., Mavridou, A., Schumann, J., Perez, I., Vlastos, P.G., Carter, C.: Dynamic assurance of autonomous systems through ground control software. In: AIAA SCITECH 2024 Forum, p.\u00a01208 (2024). https:\/\/doi.org\/10.2514\/6.2024-1208","DOI":"10.2514\/6.2024-1208"},{"key":"4_CR63","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 264\u2013276 (2009)","DOI":"10.1145\/1480881.1480915"},{"key":"4_CR64","doi-asserted-by":"publisher","unstructured":"Varanasi, S.C., et al.: TRACE: toolkit for requirements analysis, capture, and elicitation. In: NASA Formal Methods Symposium, pp. 380\u2013399. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-93706-4_22","DOI":"10.1007\/978-3-031-93706-4_22"},{"key":"4_CR65","doi-asserted-by":"publisher","unstructured":"V\u00e1zquez, G., Mavridou, A., Farrell, M., Pressburger, T., Calinescu, R.: Robotics: a new mission for FRET requirements. In: NASA Formal Methods Symposium, pp. 359\u2013376. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-60698-4_22","DOI":"10.1007\/978-3-031-60698-4_22"},{"key":"4_CR66","doi-asserted-by":"publisher","unstructured":"Wang, Z., Guzman, L.P.G., Rozier, K.Y.: WEST: interactive validation of mission-time linear temporal logic (MLTL). Sci. Comput. Program. 248 (2025). https:\/\/doi.org\/10.1016\/j.scico.2025.103365","DOI":"10.1016\/j.scico.2025.103365"},{"key":"4_CR67","doi-asserted-by":"publisher","unstructured":"Wang, Z., Kosaian, K., Rozier, K.Y.: Formally verifying a transformation from MLTL formulas to regular expressions. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 254\u2013275. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_13","DOI":"10.1007\/978-3-031-90643-5_13"},{"key":"4_CR68","doi-asserted-by":"publisher","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 (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_10","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-032-28079-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:06Z","timestamp":1781191986000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_4","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"}}]}}