{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:01:46Z","timestamp":1781193706105,"version":"3.54.1"},"publisher-location":"Cham","reference-count":21,"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_26","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:31:39Z","timestamp":1781191899000},"page":"549-566","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Runtime Verification of\u00a0Avionics Systems Using Level-D Flight Simulator Data and\u00a0NASA\/JPL\u2019s F Prime"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9732-1622","authenticated-orcid":false,"given":"Maria C.","family":"Moreno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"issue":"1","key":"26_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10009-009-0131-4","volume":"12","author":"Y Ait Ameur","year":"2010","unstructured":"Ait Ameur, Y., Boniol, F., Wiels, V.: Toward a wider use of formal methods for aerospace systems design and verification. Int. J. Softw. Tools Technol. Transfer 12(1), 1\u20137 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1","key":"26_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0376-0421(90)90006-6","volume":"27","author":"M Baarspul","year":"1990","unstructured":"Baarspul, M.: A review of flight simulation techniques. Prog. Aerosp. Sci. 27(1), 1\u2013120 (1990)","journal-title":"Prog. Aerosp. Sci."},{"issue":"4","key":"26_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Method. (TOSEM) 20(4), 1\u201364 (2011)","journal-title":"ACM Trans. Softw. Eng. Method. (TOSEM)"},{"issue":"1","key":"26_CR4","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0167-6423(99)00015-5","volume":"36","author":"G Berry","year":"2000","unstructured":"Berry, G., Bouali, A., Fornari, X., Ledinot, E., Nassor, E., De Simone, R.: Esterel: a formal method applied to avionic software development. Sci. Comput. Program. 36(1), 5\u201325 (2000)","journal-title":"Sci. Comput. Program."},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Bhatt, D., et al.: Opportunities and challenges for formal methods tools in the certification of avionics software. In: 2017 IEEE Aerospace Conference, pp. 1\u201320. IEEE (2017)","DOI":"10.1109\/AERO.2017.7943664"},{"key":"26_CR6","unstructured":"Bocchino, R., Canham, T., Watney, G., Reder, L., Levison, J.: F prime: an open-source framework for small-scale flight software systems (2018)"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruintjes, H., Cimatti, A., Katoen, J.P., Noll, T., Tonetta, S.: Formal methods for aerospace systems: achievements and challenges. In: Cyber-Physical System Design From an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings, pp. 133\u2013159. Springer (2017)","DOI":"10.1007\/978-981-10-4436-6_6"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Butler, R.W.: Nasa langley\u2019s research program in formal methods. In: COMPASS\u201991, Proceedings of the Sixth Annual Conference on Computer Assurance, pp. 157\u2013162. IEEE (1991)","DOI":"10.1109\/CMPASS.1991.161055"},{"key":"26_CR9","unstructured":"Comstock\u00a0Jr, J.R., Prinzel, L.J., Harrivel, A.R., Stephens, C.L., Kennedy, K.D.: Flight simulation scenarios for commercial pilot training and crew state monitoring. Tech. rep. (2020)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Halvorson, M., Thomas, L.D.: Architecture framework standardization for satellite software generation using MBSE and F prime. In: 2022 IEEE Aerospace Conference (AERO), pp. 1\u201320. IEEE (2022)","DOI":"10.1109\/AERO53065.2022.9843358"},{"issue":"4","key":"26_CR11","doi-asserted-by":"crossref","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)","journal-title":"Real-time Syst."},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 152\u2013166. Springer (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Metwally, A., Somov, A.: Designing future aerospace systems: integrating BIP formal verification into F prime framework. IEEE Access 13 (2025)","DOI":"10.1109\/ACCESS.2025.3606362"},{"key":"26_CR14","unstructured":"Miner, P., Neogi, N.: Formal methods at NASA: past, present, and future. In: 17th NASA Formal Methods Symposium (2025)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Formal verification of safety-critical aerospace systems. IEEE Aerosp. Electron. Syst. Mag. 38(5), 72\u201388 (2023)","DOI":"10.1109\/MAES.2023.3238378"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Pavel, M., et al.: Simulation fidelity assessment for rotorcraft\u2014methods and metrics sketches from the work of NATO AVT-296. In: 77th Annual Vertical Flight Society Forum and Technology Display, FORUM 2021: The Future of Vertical Flight (2021)","DOI":"10.4050\/F-0077-2021-16826"},{"issue":"1","key":"26_CR17","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1177\/1046878106299035","volume":"38","author":"A Robinson","year":"2007","unstructured":"Robinson, A., Mania, K.: Technological research challenges of flight simulation and flight instructor assessments of perceived fidelity. Simulat. Gaming 38(1), 112\u2013135 (2007)","journal-title":"Simulat. Gaming"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Rouff, C.A., Rash, J.L., Hinchey, M.G., Truszkowski, W.F.: Formal methods at NASA goddard space flight center. In: Agent Technology from a Formal Perspective, pp. 287\u2013309. Springer (2006)","DOI":"10.1007\/1-84628-271-3_10"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Souyris, J., Wiels, V., Delmas, D., Delseny, H.: Formal verification of avionics software products. In: International Symposium on Formal Methods, pp. 532\u2013546. Springer (2009)","DOI":"10.1007\/978-3-642-05089-3_34"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Taghizad, A., Tischler, M., Clark, R., Richard, S.: Extraction of flight dynamics data from level D qualification flight tests application to training simulators model fidelity enhancement. In: 77th Annual Forum & Technology Display: FORUM 2021 (2021)","DOI":"10.4050\/F-0077-2021-16827"},{"key":"26_CR21","unstructured":"Wiels, V., Delmas, R., Doose, D., Garoche, P.L., Cazin, J., Durrieu, G.: Formal verification of critical aerospace software. Aerospace Lab (4), p\u20131 (2012)"}],"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_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:31:47Z","timestamp":1781191907000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_26","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":"The author declares no competing interests relevant to this work. The use of Level-D flight simulators is limited to observational and experimental research purposes, and all data employed in this study were obtained from controlled simulation environments. The views expressed in this paper are solely those of the author and do not represent those of the aircraft manufacturers, simulator providers, or regulatory authorities. For certification and confidentiality reasons, the methodology abstracts simulator signals into canonical variables and avoids referencing proprietary interfaces, vendor names, or internal port numbers. The described setup reflects general engineering practices for integrating Level-D simulators with F\u2019, without disclosing sensitive implementation details.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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"}}]}}