{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T15:40:16Z","timestamp":1772206816865,"version":"3.50.1"},"publisher-location":"Cham","reference-count":50,"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_10","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:50Z","timestamp":1749316970000},"page":"159-179","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Streamlined, Formal Approach to\u00a0Requirements-Based Testing"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Katis","sequence":"first","affiliation":[]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[]},{"given":"Tom","family":"Pressburger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"10_CR1","unstructured":"CoCoSim: Contract-based Compositional Verification of Simulink Models. https:\/\/github.com\/NASA-SW-VnV\/cocosim"},{"key":"10_CR2","unstructured":"FRET: Formal Requirements Elicitation Tool. https:\/\/github.com\/NASA-SW-VnV\/fret"},{"key":"10_CR3","unstructured":"NASA core Flight System. https:\/\/cfs.gsfc.nasa.gov"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Aniculaesei, A., Howar, F., Denecke, P., Rausch, A.: Automated generation of requirements-based test cases for an adaptive cruise control system. In: 2018 IEEE Workshop on Validation, Analysis and Evolution of Software Tests (VST), pp. 11\u201315. IEEE (2018)","DOI":"10.1109\/VST.2018.8327150"},{"key":"10_CR5","unstructured":"Aniculaesei, A., Vorwald, A., Rausch, A.: Automated generation of requirements-based test cases for an automotive function using the SCADE toolchain. In: 11th International Conference on Adaptive and Self-Adaptive Systems and Applications (ADAPTIVE 2019), pp. 69\u201374 (2019)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Online testing of LTL properties for java code. In: Haifa Verification Conference, pp. 95\u2013111. Springer (2013)","DOI":"10.1007\/978-3-319-03077-7_7"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Benz, N., Sljivo, I., Vlastos, P.G., Woodard, A., Carter, C., Hejase, M.: The troupe system: an autonomous multi-agent rover swarm. In: AIAA SCITECH 2024 Forum, p. 2894 (2024)","DOI":"10.2514\/6.2024-2894"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Bhowmik, T., Chekuri, S.R., Do, A.Q., Wang, W., Niu, N.: The role of environment assertions in requirements-based testing. In: 2019 IEEE 27th International Requirements Engineering Conference (RE), pp. 75\u201385. IEEE (2019)","DOI":"10.1109\/RE.2019.00019"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 524\u2013542. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Bourbouh, H., Garoche, P.-L., Garion, C., Gurfinkel, A., Kahsai, T., Thirioux, X.: Automated analysis of stateflow models. In: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2017), vol. 46, pp. 144\u2013161 (2017)","DOI":"10.29007\/b8gq"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3461668","volume":"5","author":"H Bourbouh","year":"2021","unstructured":"Bourbouh, H., Garoche, P.-L., Garion, C., Thirioux, X.: From lustre to simulink: reverse compilation for embedded systems applications. ACM Trans. Cyber-Phys. Syst. 5(3), 1\u201320 (2021)","journal-title":"ACM Trans. Cyber-Phys. Syst."},{"key":"10_CR12","unstructured":"Bourbouh, H., Garoche, P.-L., Loquen, T., Noulard, \u00c9., Pagetti, C.: CoCoSim, a code generation framework for control\/command applications: an overview of CoCoSim for multi-periodic discrete simulink models. Embedded Real Time Systems (ERTS) 2020, (ARC-E-DAA-TN74591) (2020)"},{"key":"10_CR13","unstructured":"Bozzano, M., et al.: nuXmv 2.0. 0 user manual. Fondazione Bruno Kessler, Technical Report, Trento, Italy (2019)"},{"issue":"1","key":"10_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/32.210303","volume":"19","author":"RW Butler","year":"1993","unstructured":"Butler, R.W., Finelli, G.B.: The infeasibility of quantifying the reliability of life-critical real-time software. IEEE Trans. Softw. Eng. 19(1), 3\u201312 (1993)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Canny, P., Nascimento, G.C.: An approachable and partially automated specification modeling workflow. In: AIAA SCITECH 2024 Forum, p. 0159 (2024)","DOI":"10.2514\/6.2024-0159"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De\u00a0Nicola, R., K\u00fchn, E. (eds.) Software Engineering and Formal Methods, pp. 347\u2013366. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-41591-8_24"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: International Conference on Computer Aided Verification, pp. 510\u2013517. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Cimatti, A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, 27\u201331 July 2002, Proceedings 14, pp. 359\u2013364. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"10_CR19","unstructured":"Elliott, C., Tallant, G., Stanfill, P.: An example set of cyber-physical V &V challenges for S5. In: Air Force Research Laboratory Safe and Secure Systems and Software Symposium (S5) Conference (2016)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Engels, A., Feijs, L., Mauw, S.: Test generation for intelligent networks using model checking. In: Tools and Algorithms for the Construction and Analysis of Systems: Third International Workshop, TACAS 1997 Enschede, The Netherlands, 2\u20134 April 1997, Proceedings 3, pp. 384\u2013398. Springer (1997)","DOI":"10.1007\/BFb0035401"},{"key":"10_CR21","doi-asserted-by":"crossref","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: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, 16\u201318 May 2017, Proceedings 9, pp. 420\u2013426. Springer (2017)","DOI":"10.1007\/978-3-319-57288-8_30"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Fraser, G., Gargantini, A.: An evaluation of specification based test generation techniques using model checkers. In: 2009 Testing: Academic and Industrial Conference-Practice and Research Techniques, pp. 72\u201381. IEEE (2009)","DOI":"10.1109\/TAICPART.2009.20"},{"issue":"6","key":"10_CR23","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1145\/318774.318939","volume":"24","author":"A Gargantini","year":"1999","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. ACM SIGSOFT Softw. Eng. Notes 24(6), 146\u2013162 (1999)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"10_CR24","unstructured":"Giannakopoulou, D., Mavridou, A., Pressburger, T., Rhein, J., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: REFSQ (2020)"},{"key":"10_CR25","doi-asserted-by":"publisher","first-page":"106590","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)","journal-title":"Inf. Softw. Technol."},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Belt, J., Robby, Legg, J., Stewart, D., Carpenter, T.: Automated property-based testing from AADL component contracts. In: International Conference on Formal Methods for Industrial Critical Systems, pp. 131\u2013150. Springer (2023)","DOI":"10.1007\/978-3-031-43681-9_8"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Hejase, M., Katis, A., Mavridou, A.: Design, formalization, and verification of decision making for intelligent systems. In: AIAA SCITECH 2024 Forum, p. 2409 (2024)","DOI":"10.2514\/6.2024-2409"},{"key":"10_CR28","unstructured":"Jahier, E., Raymond, P., Halbwachs, N.: The lustre V6 reference manual. Verimag, Grenoble (2016)"},{"key":"10_CR29","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-031-13188-2_24"},{"key":"10_CR30","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Int. J. Softw. Tools Technol. Transf. 4, 224\u2013233 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Langenfeld, V., Dietsch, D., Westphal, B., Hoenicke, J., Post, A.: Scalable analysis of real-time requirements. In: 2019 IEEE 27th International Requirements Engineering Conference (RE), pp. 234\u2013244. IEEE (2019)","DOI":"10.1109\/RE.2019.00033"},{"issue":"2","key":"10_CR32","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/3591335.3591338","volume":"42","author":"D Larraz","year":"2023","unstructured":"Larraz, D., Viswanathan, A., Tinelli, C., Laurent, M.: Beyond model checking of idealized Lustre in kind 2. Ada Lett. 42(2), 40\u201344 (2023)","journal-title":"Ada Lett."},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Li, M., et al.: Requirements-based automated test generation for safety critical software. In: 2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC), pp. 1\u201310. IEEE (2019)","DOI":"10.1109\/DASC43569.2019.9081726"},{"key":"10_CR34","unstructured":"Mavridou, A., Bourbouh, H., Garoche, P.L., Giannakopoulou, D., Pessburger, T., Schumann, J.: Bridging the gap between requirements and simulink model analysis. In: Joint 26th International Conference on Requirements Engineering: Foundation for Software Quality Workshops, Doctoral Symposium, Live Studies Track, and Poster Track (2020)"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Mavridou, A., et al.: The ten lockheed martin cyber-physical challenges: formalized, analyzed, and explained. In: 2020 IEEE 28th International Requirements Engineering Conference (RE), pp. 300\u2013310. IEEE (2020)","DOI":"10.1109\/RE48521.2020.00040"},{"key":"10_CR36","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s00766-019-00316-x","volume":"24","author":"A Moitra","year":"2019","unstructured":"Moitra, A., et al.: Automating requirements analysis and test case generation. Requirements Eng. 24, 341\u2013364 (2019)","journal-title":"Requirements Eng."},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Murugesan, A., et al: Are we there yet? Determining the adequacy of formalized requirements and test suites. In: NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, 27\u201329 April 2015, Proceedings 7, pp. 279\u2013294. Springer (2015)","DOI":"10.1007\/978-3-319-17524-9_20"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Pulina, L., Tacchella, A., Vuotto, S.: Automated requirements-based testing of black-box reactive systems. In: NASA Formal Methods: 12th International Symposium, NFM 2020, Moffett Field, CA, USA, 11\u201315 May 2020, Proceedings 12, pp. 153\u2013169. Springer (2020)","DOI":"10.1007\/978-3-030-55754-6_9"},{"key":"10_CR39","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, L., Wickstr\u00f6m, O.: QuickStrom: property-based acceptance testing with LTL specifications. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 1025\u20131038 (2022)","DOI":"10.1145\/3519939.3523728"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Pecheur, C., Raimondi, F., Brat, G.: A formal analysis of requirements-based testing. In: Proceedings of the 18th International Symposium on Software Testing and Analysis, pp. 47\u201356 (2009)","DOI":"10.1145\/1572272.1572279"},{"key":"10_CR41","doi-asserted-by":"crossref","unstructured":"Perez, I., Mavridou, A., Pressburger, T., Goodloe, A., Giannakopoulou, D.: Automated translation of natural language requirements to runtime monitors. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 387\u2013395. Springer, Cham (2022)","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"10_CR42","doi-asserted-by":"crossref","unstructured":"Pilaud, D., albwachs, N., Plaice, J.A.: Lustre: a declarative language for programming synchronous systems. In: Proceedings of the 14th Annual ACM Symposium on Principles of Programming Languages (14th POPL 1987), New York, NY, vol. 178, p. 188. Citeseer, ACM (1987)","DOI":"10.1145\/41625.41641"},{"key":"10_CR43","doi-asserted-by":"crossref","unstructured":"Rajan, A., Whalen, M., Staats, M., Heimdahl, M.P.E.: Requirements coverage as an adequacy measure for conformance testing. In: International Conference on Formal Engineering Methods, pp. 86\u2013104. Springer (2008)","DOI":"10.1007\/978-3-540-88194-0_8"},{"key":"10_CR44","doi-asserted-by":"crossref","unstructured":"Rayadurgam, S., Heimdahl, M.P.E.: Coverage based test-case generation using model checkers. In: Proceedings of the Eighth Annual IEEE International Conference and Workshop On the Engineering of Computer-Based Systems-ECBS 2001, pp. 83\u201391. IEEE (2001)","DOI":"10.1109\/ECBS.2001.922409"},{"key":"10_CR45","doi-asserted-by":"publisher","first-page":"111518","DOI":"10.1016\/j.jss.2022.111518","volume":"195","author":"A Salahirad","year":"2023","unstructured":"Salahirad, A., Gay, G., Mohammadi, E.: Mapping the structure and evolution of software testing research over the past three decades. J. Syst. Softw. 195, 111518 (2023)","journal-title":"J. Syst. Softw."},{"key":"10_CR46","doi-asserted-by":"crossref","unstructured":"Sljivo, I., Perez, I., Mavridou, A., Schumann, J., Vlastos, P.G., Carter, C.: Dynamic assurance of autonomous systems through ground control software. In: AIAA SCITECH 2024 Forum, p. 1208 (2024)","DOI":"10.2514\/6.2024-1208"},{"key":"10_CR47","unstructured":"Staats, M., Whalen, M., Rajan, A., Heimdahl, M.: Coverage metrics for requirements-based testing: evaluation of effectiveness (2010)"},{"key":"10_CR48","doi-asserted-by":"crossref","unstructured":"Sun, Y., Huang, X., Kroening, D., Sharp, J., Hill, M., Ashmore, R.: Structural test coverage criteria for deep neural networks. ACM Trans. Embed. Comput. Syst. 18(5s) (2019)","DOI":"10.1145\/3358233"},{"key":"10_CR49","unstructured":"Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: 2004 Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration, IRI 2004, pp. 493\u2013498. IEEE (2004)"},{"key":"10_CR50","doi-asserted-by":"crossref","unstructured":"Whalen, M.W., Rajan, A., Heimdahl, M.P.E., Miller, S.P.: Coverage metrics for requirements-based testing. In: Proceedings of the 2006 International Symposium on Software Testing and Analysis, ISSTA 2006, pp. 25\u201336. Association for Computing Machinery, New York (2006)","DOI":"10.1145\/1146238.1146242"}],"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_10","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_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_10","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"}}]}}