{"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":1781193869595,"version":"3.54.1"},"publisher-location":"Cham","reference-count":49,"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_6","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:19Z","timestamp":1781191999000},"page":"120-141","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Hardware-in-the-Loop Validation of\u00a0Formal Models: An Application to\u00a0AI-Controlled Drones"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2556-5553","authenticated-orcid":false,"given":"Fabian","family":"Vu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4228-404X","authenticated-orcid":false,"given":"Jan","family":"Gruteser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-9560","authenticated-orcid":false,"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6722-6296","authenticated-orcid":false,"given":"David","family":"Gele\u00dfus","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Miles","family":"Vella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"6_CR1","unstructured":"FMI Standard (2025). https:\/\/fmi-standard.org\/. Accessed 9 Dec 2025"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (2005). https:\/\/doi.org\/10.1017\/CBO9780511624162","DOI":"10.1017\/CBO9780511624162"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010). https:\/\/doi.org\/10.1017\/CBO9781139195881","DOI":"10.1017\/CBO9781139195881"},{"issue":"6","key":"6_CR4","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Aljalbout, E., et al.: The Reality Gap in Robotics: Challenges, Solutions, and Best Practices (2025). https:\/\/doi.org\/10.48550\/arXiv.2510.20808","DOI":"10.48550\/arXiv.2510.20808"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Bacic, M.: On hardware-in-the-loop simulation. In: Proceedings of the 44th IEEE Conference on Decision and Control, pp. 3194\u20133198. IEEE (2005). https:\/\/doi.org\/10.1109\/CDC.2005.1582653","DOI":"10.1109\/CDC.2005.1582653"},{"key":"6_CR7","doi-asserted-by":"publisher","DOI":"10.1145\/3689374","author":"MH ter Beek","year":"2024","unstructured":"ter Beek, M.H., et al.: Formal methods in industry. Formal Aspects Comput. (2024). https:\/\/doi.org\/10.1145\/3689374","journal-title":"Formal Aspects Comput."},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-030-85248-1_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"J Bendisposto","year":"2021","unstructured":"Bendisposto, J., Gele\u00dfus, D., Jansing, Y., Leuschel, M., P\u00fctz, A., Vu, F., Werth, M.: ProB2-UI: a Java-based user interface for ProB. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 193\u2013201. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_12"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Bert, D., Boulm\u00e9, S., Potet, M.L., Requet, A., Voisin, L.: Adaptable translator of b specifications to embedded C programs. In: Proceedings FME, pp. 94\u2013113. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_7","DOI":"10.1007\/978-3-540-45236-2_7"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Bonfanti, S., Carissoni, M., Gargantini, A., Mashkoor, A.: Asm2C++: a tool for code generation from abstract state machines to arduino. In: NASA Formal Methods, pp. 295\u2013301. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_21","DOI":"10.1007\/978-3-319-57288-8_21"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Bonfanti, S., Gargantini, A.: The mechanical lung ventilator case study. In: Proceedings ABZ, pp. 281\u2013288. LNCS 14759, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63790-2_23","DOI":"10.1007\/978-3-031-63790-2_23"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Bonfanti, S., Riccobene, E., Scandurra, P.: Formal specification and validation of the MVM-Adapt system using Compositional I\/O Abstract State Machines. Sci. Comput. Program. 244(C) (2025). https:\/\/doi.org\/10.1016\/j.scico.2025.103299","DOI":"10.1016\/j.scico.2025.103299"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-15075-8_1","volume-title":"Formal Methods: Foundations and Applications","author":"R Bonichon","year":"2015","unstructured":"Bonichon, R., D\u00e9harbe, D., Lecomte, T., Medeiros, V.: LLVM-based code generation for B. In: Braga, C., Mart\u00ed-Oliet, N. (eds.) SBMF 2014. LNCS, vol. 8941, pp. 1\u201316. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15075-8_1"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-39698-4_5","volume-title":"Theories of Programming and Formal Methods","author":"M Butler","year":"2013","unstructured":"Butler, M., Maamria, I.: Practical theory extension in event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67\u201381. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39698-4_5"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Cavalcanti, A.: Modelling and verification of robotic platforms for simulation using RoboStar technology. In: Proceedings ABZ, pp.\u00a03\u20135 (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_1","DOI":"10.1007\/978-3-030-48077-6_1"},{"issue":"19","key":"6_CR16","doi-asserted-by":"publisher","first-page":"2447","DOI":"10.3390\/electronics10192447","volume":"10","author":"Y Chung","year":"2021","unstructured":"Chung, Y., Yang, Y.P.: Hardware-in-the-loop simulation of self-driving electric vehicles by dynamic path planning and model predictive control. Electronics 10(19), 2447 (2021). https:\/\/doi.org\/10.3390\/electronics10192447","journal-title":"Electronics"},{"key":"6_CR17","unstructured":"ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2016). http:\/\/www.atelierb.eu\/"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Edmunds, A., Rezazadeh, A., Butler, M.: Formal modelling for ada implementations: tasking Event-B. In: Reliable Software Technologies \u2013 Ada-Europe 2012, pp. 119\u2013132. Springer (2012). 978-3-642-30598-6_9","DOI":"10.1007\/978-3-642-30598-6_9"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Fang, A., Kress-Gazit, H.: High-level, collaborative task planning grammar and execution for heterogeneous agents. In: Proceedings AAMAS, pp. 544\u2013552. International Foundation for Autonomous Agents and Multiagent Systems\/ACM (2024). https:\/\/doi.org\/10.5555\/3635637.3662905","DOI":"10.5555\/3635637.3662905"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Gruteser, J., Leuschel, M., Wunsch, S.: Type-safe validation of XML railway data in B. In: Journeys Between Formal Methods and the Railway Industry \u2013 Essays Dedicated to Alessandro Fantechi on the Occasion of His 70th Birthday, pp. 292\u2013313. Springer (2026). https:\/\/doi.org\/10.1007\/978-3-032-12484-5_16","DOI":"10.1007\/978-3-032-12484-5_16"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Gruteser, J., Ro\u00dfbach, J., Vu, F., Leuschel, M.: Using formal models, safety shields and certified control to validate AI-based train systems. In: Proceedings FMAS, pp. 151\u2013159. EPTCS 411, Open Publishing Association (2024). https:\/\/doi.org\/10.4204\/EPTCS.411.10","DOI":"10.4204\/EPTCS.411.10"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Hanselmann, H.: Hardware-in-the-loop simulation testing and its integration into a CACSD toolset. In: Proceedings of Joint Conference on Control Applications Intelligent Control and Computer Aided Control System Design, pp. 152\u2013156. IEEE (1996). https:\/\/doi.org\/10.1109\/CACSD.1996.555253","DOI":"10.1109\/CACSD.1996.555253"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-30729-4_3","volume-title":"Integrated Formal Methods","author":"D Hansen","year":"2012","unstructured":"Hansen, D., Leuschel, M.: Translating TLA\u2009+\u2009 to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Hansen, D., et al.: Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model. Int. J. Softw. Tools Technol. Transfer 22(3), 315\u2013332 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00551-6","DOI":"10.1007\/s10009-020-00551-6"},{"key":"6_CR25","unstructured":"Hintjens, P.: ZeroMQ: Messaging for Many Applications. O\u2019Reilly Media Inc. (2013)"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Hoang, T.S., Snook, C., Ladenberger, L., Butler, M.: Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion studio, and co-simulation. In: Proceedings ABZ, pp. 360\u2013375. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_31","DOI":"10.1007\/978-3-319-33600-8_31"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Ingalalli, A., Satheesh, H., Kande, M.: Platform for hardware in loop simulation. In: 2016 International Symposium on Power Electronics, Electrical Drives, Automation and Motion (SPEEDAM), pp. 41\u201346. IEEE (2016). https:\/\/doi.org\/10.1109\/SPEEDAM.2016.7525843","DOI":"10.1109\/SPEEDAM.2016.7525843"},{"issue":"5","key":"6_CR28","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1016\/S0967-0661(98)00205-6","volume":"7","author":"R Isermann","year":"1999","unstructured":"Isermann, R., Schaffnit, J., Sinsel, S.: Hardware-in-the-loop simulation for the design and testing of engine-control systems. Control. Eng. Pract. 7(5), 643\u2013653 (1999). https:\/\/doi.org\/10.1016\/S0967-0661(98)00205-6","journal-title":"Control. Eng. Pract."},{"issue":"11","key":"6_CR29","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/3715958","volume":"68","author":"B K\u00f6nighofer","year":"2025","unstructured":"K\u00f6nighofer, B., Bloem, R., Jansen, N., Junges, S., Pranger, S.: Shields for safe reinforcement learning. Commun. ACM 68(11), 80\u201390 (2025). https:\/\/doi.org\/10.1145\/3715958","journal-title":"Commun. ACM"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"K\u00f6rner, P., Bendisposto, J., Dunkelau, J., Krings, S., Leuschel, M.: Integrating formal specifications into applications: the ProB Java API. Formal Methods Syst. Des. 58(1), 160\u2013187 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00351-3","DOI":"10.1007\/s10703-020-00351-3"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-91271-4_6","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"S Krings","year":"2018","unstructured":"Krings, S., Schmidt, J., Brings, C., Frappier, M., Leuschel, M.: A translation from alloy to B. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 71\u201386. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91271-4_6"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Leitner, J.: Space technology transition using hardware in the loop simulation. In: 1996 IEEE Aerospace Applications Conference. Proceedings. vol.\u00a02, pp. 303\u2013311. IEEE (1996). https:\/\/doi.org\/10.1109\/AERO.1996.495985","DOI":"10.1109\/AERO.1996.495985"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-030-76020-5_9","volume-title":"Logic, Computation and Rigorous Methods","author":"M Leuschel","year":"2021","unstructured":"Leuschel, M.: Spot the difference: a detailed comparison between B and event-B. In: Raschke, A., Riccobene, E., Schewe, K.-D. (eds.) Logic, Computation and Rigorous Methods. LNCS, vol. 12750, pp. 147\u2013172. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76020-5_9"},{"issue":"2","key":"6_CR34","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transfer 10(2), 185\u2013203 (2008). https:\/\/doi.org\/10.1007\/s10009-007-0063-9","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-33600-8_29","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Mashkoor","year":"2016","unstructured":"Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329\u2013343. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_29"},{"issue":"4","key":"6_CR36","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/s11334-021-00416-4","volume":"18","author":"K Morris","year":"2022","unstructured":"Morris, K., Snook, C., Hoang, T.S., Hulette, G., Armstrong, R., Butler, M.: Formal verification and validation of run-to-completion style state charts using Event-B. Innov. Syst. Softw. Eng. 18(4), 523\u2013541 (2022). https:\/\/doi.org\/10.1007\/s11334-021-00416-4","journal-title":"Innov. Syst. Softw. Eng."},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480\u2013500. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_25"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"Riccobene, E., Scandurra, P.: Exploring the concept of abstract state machines for system runtime enforcement. In: Proceedings ABZ, pp. 244\u2013247. LNCS 12071 (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_18","DOI":"10.1007\/978-3-030-48077-6_18"},{"key":"6_CR39","unstructured":"Savicks, V., Butler, M., Colley, J.: Co-simulating event-B and continuous models via FMI. In: Proceedings of the 2014 Summer Simulation Multiconference. Society for Computer Simulation International (2014)"},{"issue":"1","key":"6_CR40","doi-asserted-by":"publisher","first-page":"205395172413098","DOI":"10.1177\/20539517241309884","volume":"12","author":"J Steinhoff","year":"2025","unstructured":"Steinhoff, J., Hind, S.: Simulation and the reality gap: moments in a prehistory of synthetic data. Big Data Soc. 12(1), 20539517241309884 (2025). https:\/\/doi.org\/10.1177\/20539517241309884","journal-title":"Big Data Soc."},{"key":"6_CR41","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT press (2018)"},{"key":"6_CR42","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.simpat.2018.12.005","volume":"92","author":"C Thule","year":"2019","unstructured":"Thule, C., Lausdahl, K., Gomes, C., Meisl, G., Larsen, P.G.: Maestro: the INTO-CPS co-simulation framework. Simul. Model. Pract. Theory 92, 45\u201361 (2019). https:\/\/doi.org\/10.1016\/j.simpat.2018.12.005","journal-title":"Simul. Model. Pract. Theory"},{"key":"6_CR43","doi-asserted-by":"publisher","unstructured":"Vu, F., Dunkelau, J., Leuschel, M.: Validation of reinforcement learning agents and safety shields with ProB. In: Proceedings NFM. pp. 279\u2013297. LNCS, vol. 14627. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-60698-4_16","DOI":"10.1007\/978-3-031-60698-4_16"},{"key":"6_CR44","doi-asserted-by":"publisher","unstructured":"Vu, F., Happe, C., Leuschel, M.: Generating interactive documents for domain-specific validation of formal models. Int. J. Softw. Tools Technol. Transfer 26(2), 147\u2013168 (2024). https:\/\/doi.org\/10.1007\/s10009-024-00739-0","DOI":"10.1007\/s10009-024-00739-0"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"Vu, F., Leuschel, M.: Validation of formal models by interactive simulation. In: Proceedings ABZ, pp. 59\u201369. LNCS 14010 (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_5","DOI":"10.1007\/978-3-031-33163-3_5"},{"key":"6_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-030-77543-8_6","volume-title":"Rigorous State-Based Methods","author":"F Vu","year":"2021","unstructured":"Vu, F., Leuschel, M., Mashkoor, A.: Validation of formal models by timed probabilistic simulation. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 81\u201396. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_6"},{"key":"6_CR47","doi-asserted-by":"crossref","unstructured":"Watkins, C.J., Dayan, P.: Q-learning. Mach. Learn. 8, 279\u2013292 (1992). https:\/\/doi.org\/10.1007\/BF00992698","DOI":"10.1007\/BF00992698"},{"key":"6_CR48","doi-asserted-by":"publisher","unstructured":"Werth, M., Leuschel, M.: VisB: a lightweight tool to visualize formal models with SVG graphics. In: Proceedings ABZ, pp. 260\u2013265. LNCS 12071. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_21","DOI":"10.1007\/978-3-030-48077-6_21"},{"key":"6_CR49","doi-asserted-by":"publisher","unstructured":"Wong, K.W., Ehlers, R., Kress-Gazit, H.: Resilient, provably-correct, and high-level robot behaviors. IEEE Trans. Robotics 34(4), 936\u2013952 (2018). https:\/\/doi.org\/10.1109\/TRO.2018.2830353","DOI":"10.1109\/TRO.2018.2830353"}],"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_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:22Z","timestamp":1781192002000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_6","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"}}]}}