{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T19:01:55Z","timestamp":1783018915817,"version":"3.54.6"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Validation is a central activity when developing formal specifications. Similarly to coding, a possible validation technique is to define upfront test cases or scenarios that a future specification should satisfy or not. Unfortunately, specifying such test cases is burdensome and error prone, which could cause users to skip this validation task. This paper reports the results of an empirical evaluation of using pre-trained large language models (LLMs) to automate the generation of test cases from natural language requirements. In particular, we focus on test cases for structural requirements of simple domain models formalized in the Alloy specification language. Our evaluation focuses on the state-of-the-art GPT-5 model, but results from other closed- and open-source LLMs are also reported. The results show that, in this context, GPT-5 is already quite effective at generating positive (and negative) test cases that are syntactically correct and that satisfy (or not) the given requirement, and that can detect many wrong specifications written by humans.<\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_15","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:49:56Z","timestamp":1779032996000},"page":"279-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Validating Formal Specifications with\u00a0LLM-Generated Test Cases"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2714-8027","authenticated-orcid":false,"given":"Alcino","family":"Cunha","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4817-948X","authenticated-orcid":false,"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"issue":"5","key":"15_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10664-025-10687-1","volume":"30","author":"M Alhanahnah","year":"2025","unstructured":"Alhanahnah, M., Rashedul Hasan, M., Xu, L., Bagheri, H.: An empirical evaluation of pre-trained large language models for repairing declarative formal specifications. Empir. Softw. Eng. 30(5), 1\u201338 (2025)","journal-title":"Empir. Softw. Eng."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Arora, C., Herda, T., Homm, V.: Generating test scenarios from NL requirements using retrieval-augmented LLMs: an industrial study. In: 32nd International Requirements Engineering Conference, pp. 240\u2013251. IEEE (2024)","DOI":"10.1109\/RE59067.2024.00031"},{"issue":"11","key":"15_CR3","doi-asserted-by":"publisher","first-page":"6581","DOI":"10.1109\/TSMC.2024.3392930","volume":"54","author":"C Chang","year":"2024","unstructured":"Chang, C., Wang, S., Zhang, J., Ge, J., Li, L.: LLMScenario: large language model driven scenario generation. IEEE Trans. Syst. Man Cybern. Syst. 54(11), 6581\u20136594 (2024)","journal-title":"IEEE Trans. Syst. Man Cybern. Syst."},{"key":"15_CR4","unstructured":"Cunha, A., Macedo, N., Brunel, J., Chemouil, D.: Practical Alloy: a hands-on guide to formal software design (2025). https:\/\/practicalalloy.github.io\/"},{"key":"15_CR5","unstructured":"Hong, Y., Jiang, S., Fu, Y., Khurshid, S.: On the effectiveness of large language models in writing Alloy formulas. arXiv preprint arXiv:2502.15441 (2025)"},{"key":"15_CR6","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2012)"},{"issue":"9","key":"15_CR7","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019)","journal-title":"Commun. ACM"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Korraprolu, B.R., Pinninti, P., Reddy, Y.R.: Test case generation for requirements in natural language \u2013 an LLM comparison study. In: 18th Innovations in Software Engineering Conference, pp. 9:1\u20139:5. ACM (2025)","DOI":"10.1145\/3717383.3717389"},{"key":"15_CR9","unstructured":"Lamport, L.: Specifying Systems, vol.\u00a0388. Addison-Wesley (2002)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 373\u2013383. ACM (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Macedo, N., Cunha, A.: Alloy4Fun semantic entries (2025). https:\/\/doi.org\/10.5281\/zenodo.17392203","DOI":"10.5281\/zenodo.17392203"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Macedo, N., Cunha, A., Paiva, A.C.R.: Alloy4Fun dataset for 2024\/25 (2025). https:\/\/doi.org\/10.5281\/zenodo.17390557","DOI":"10.5281\/zenodo.17390557"},{"key":"15_CR13","doi-asserted-by":"publisher","first-page":"102690","DOI":"10.1016\/j.scico.2021.102690","volume":"211","author":"N Macedo","year":"2021","unstructured":"Macedo, N., et al.: Experiences on teaching Alloy with an automated assessment platform. Sci. Comput. Program. 211, 102690 (2021)","journal-title":"Sci. Comput. Program."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Mashkoor, A., Leuschel, M., Egyed, A.: Validation obligations: a novel approach to check compliance between requirements and their formal specification. In: 43rd International Conference on Software Engineering: New Ideas and Emerging Results, pp.\u00a01\u20135. IEEE (2021)","DOI":"10.1109\/ICSE-NIER52604.2021.00009"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Masuda, S., Kouzawa, S., Sezai, K., Suhara, H., Hiruta, Y., Kudou, K.: Generating high-level test cases from requirements using LLM: an industry study. arXiv preprint arXiv:2510.03641 (2025)","DOI":"10.1109\/ACDSA67686.2026.11467785"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Pan, F., Petrovic, N., Zolfaghari, V., Wen, L., Knoll, A.: LLM-enabled instance model generation. arXiv preprint arXiv:2503.22587 (2025)","DOI":"10.1109\/MODELS-C68889.2025.00082"},{"issue":"1","key":"15_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1109\/TSE.2023.3334955","volume":"50","author":"M Sch\u00e4fer","year":"2023","unstructured":"Sch\u00e4fer, M., Nadi, S., Eghbali, A., Tip, F.: An empirical evaluation of using large language models for automated unit test generation. IEEE Trans. Software Eng. 50(1), 85\u2013105 (2023)","journal-title":"IEEE Trans. Software Eng."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Wang, K., Khurshid, S.: AUnit: a test automation tool for Alloy. In: 11th International Conference on Software Testing, Verification and Validation, pp. 398\u2013403. IEEE (2018)","DOI":"10.1109\/ICST.2018.00047"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: 10th International Conference on Software Testing, Verification and Validation, pp. 264\u2013275. IEEE (2017)","DOI":"10.1109\/ICST.2017.31"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. In: 21st International Conference on Computer Aided Verification, LNCS, vol.\u00a05643, pp. 709\u2013714. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: ARepair: a repair framework for Alloy. In: 41st International Conference on Software Engineering: Companion Proceedings, pp. 103\u2013106. IEEE (2019)","DOI":"10.1109\/ICSE-Companion.2019.00049"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Xue, Z., et al.: LLM4Fin: Fully automating LLM-powered test case generation for fintech software acceptance testing. In: 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 1643\u20131655. ACM (2024)","DOI":"10.1145\/3650212.3680388"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Yang, L., et\u00a0al.: On the evaluation of large language models in unit test generation. In: 39th IEEE\/ACM International Conference on Automated Software Engineering, pp. 1607\u20131619. ACM (2024)","DOI":"10.1145\/3691620.3695529"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Yang, Z., Huang, R., Cui, C., Niu, N., Towey, D.: Requirements-based test generation: a comprehensive survey. ACM Trans. Softw. Eng. Methodol. (2025), to appear","DOI":"10.1145\/3771727"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Zhao, M., Tao, R., Huang, Y., Shi, J., Qin, S., Yang, Y.: NL2CTL: automatic generation of formal requirements specifications via large language models. In: 25th International Conference on Formal Engineering Methods, LNCS, vol. 15394, pp. 1\u201317. Springer (2024)","DOI":"10.1007\/978-981-96-0617-7_1"},{"issue":"3","key":"15_CR26","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1002\/smr.554","volume":"24","author":"S Zugal","year":"2012","unstructured":"Zugal, S., Pinggera, J., Weber, B.: Toward enhanced life-cycle support for declarative processes. J. Softw. Evol. Process 24(3), 285\u2013302 (2012)","journal-title":"J. Softw. Evol. Process"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Zuo, X., et al.: PAT-Agent: autoformalization for model checking. arXiv preprint arXiv:2509.23675 (2025)","DOI":"10.1109\/ASE63991.2025.00176"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T17:54:41Z","timestamp":1783014881000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_15","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":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}