{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:50Z","timestamp":1783545350850,"version":"3.55.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","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>\n                    Requirement defects are a major source of late-stage failures in automotive systems, yet rigorous validation is rarely applied during early development. While formal methods offer strong guarantees, their adoption at the requirements level is limited by high formalization cost and expertise barriers. We present an industry-oriented, shift-left verification approach that integrates Large Language Models (LLMs) with formal methods to enable requirements-level validation. Requirements are classified and decomposed by LLMs, translated into CSP system models and assertions, and refined through a CEGAR-inspired loop using the FDR4 model checker. Validation is decomposed into requirement\u2013assertion pairs supported by natural-language back-translations and confidence scores, preserving expert control without manual formal modeling. Domain knowledge\u2013based validation further leverages historical defect data to identify implicit requirement gaps. We evaluate the approach on three real-world automotive case studies. Results show high automation for small-to-medium systems (80\u2013100% synthesis success for up to\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\sim 60$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>\u223c<\/mml:mo>\n                            <mml:mn>60<\/mml:mn>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    requirements), effective expert validation guided by LLM confidence estimates, and 100% detection of known historical defects alongside 22 novel gaps. The workflow completes within 10\u201335\u00a0min per project at negligible cost (\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$&lt;8$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>&lt;<\/mml:mo>\n                            <mml:mn>8<\/mml:mn>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    per project), with limited expert effort. Our results demonstrate that LLM+formal method hybridization can provide scalable, rigorous, and industrially viable requirements-level verification, supporting practical shift-left adoption in automotive systems.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_31","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:20:42Z","timestamp":1779024042000},"page":"631-650","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Shift-Left Requirements Verification: Integrating LLMs and\u00a0Formal Methods for\u00a0Automotive Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-5667-4227","authenticated-orcid":false,"given":"Zipong","family":"Lim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0360-2248","authenticated-orcid":false,"given":"Bozhi","family":"Wu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5081-6712","authenticated-orcid":false,"given":"Yon Shin","family":"Teo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9726-3434","authenticated-orcid":false,"given":"Shang-wei","family":"Lin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4562-8208","authenticated-orcid":false,"given":"Yi","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Bashir, S., et al.: Requirements ambiguity detection and explanation with LLMs: an industrial study. In: International Conference on Software Maintenance and Evolution (2025)","DOI":"10.1109\/ICSME64153.2025.00063"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Binkhonain, M., Alfayez, R.: Are prompts all you need? Evaluating prompt-based large language models (LLM)s for software requirements classification. In: Requirements Engineering, pp. 1\u201321 (2025)","DOI":"10.1007\/s00766-025-00451-8"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Boehm, B., Basili, V.R.: Software defect reduction top 10 list. Found. Empir. Softw. Eng. Legacy Victor R. Basili 426(37), 426\u2013431 (2005)","DOI":"10.1007\/3-540-27662-9_26"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 54\u201356. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0058022"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244\u2013263 (1986)","DOI":"10.1145\/5397.5399"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Accurate theorem proving for program verification. In: International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, pp. 96\u2013114. Springer (2004)","DOI":"10.1007\/11925040_7"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: International Conference on Security in Pervasive Computing, pp. 193\u2013209. Springer (2005)","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"31_CR9","unstructured":"Fuchs, N.E., Schwitter, R.:. Attempto controlled English (ace). arXiv preprint cmp-lg\/9603003 (1996)"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K., (eds.), Tools and Algorithms for the Construction and Analysis of Systems, vol. 8413, LNCS, pp. 187\u2013201 (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Green, C.: Application of theorem proving to problem solving. In: Readings iN Artificial Intelligence, pp. 202\u2013222. Elsevier (1981)","DOI":"10.1016\/B978-0-934613-03-3.50019-2"},{"issue":"3","key":"31_CR12","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/s10664-025-10619-z","volume":"30","author":"S Hassani","year":"2025","unstructured":"Hassani, S., Sabetzadeh, M., Amyot, D.: An empirical study on LLM-based classification of requirements-related provisions in food-safety regulations. Empir. Softw. Eng. 30(3), 72 (2025)","journal-title":"Empir. Softw. Eng."},{"issue":"8","key":"31_CR13","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"issue":"4","key":"31_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. (CSUR) 41(4), 1\u201354 (2009)","journal-title":"ACM Comput. Surv. (CSUR)"},{"issue":"OOPSLA1","key":"31_CR15","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1145\/3649828","volume":"8","author":"Yu Haonan Li","year":"2024","unstructured":"Haonan Li, Yu., Hao, Y.Z., Qian, Z.: Enhancing static analysis for practical bug detection: an LLM-integrated approach. Proc. ACM Program. Lang. 8(OOPSLA1), 474\u2013499 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Li, H., et al.: Retrieval-augmented fine-tuning for improving retrieve-and-edit based assertion generation. IEEE Trans. Softw. Eng. (2025)","DOI":"10.1109\/TSE.2025.3558403"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Lin, S.: LLM-driven adaptive source\u2013CSink identification and false positive mitigation for static analysis. In: Proceedings of the 2025 8th International Conference on Computer Information Science and Artificial Intelligence, pp. 281\u2013285 (2025)","DOI":"10.1145\/3773365.3773410"},{"key":"31_CR18","doi-asserted-by":"publisher","first-page":"54932","DOI":"10.52202\/079017-1742","volume":"37","author":"X Lin","year":"2024","unstructured":"Lin, X., et al.: FVEL: interactive formal verification environment with large language models via theorem proving. Adv. Neural. Inf. Process. Syst. 37, 54932\u201354946 (2024)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Mavin, A., Wilkinson, P., Harwood, A., Novak, M.: Easy approach to requirements syntax (ears). In: 2009 17th IEEE International Requirements Engineering Conference, pp. 317\u2013322. IEEE (2009)","DOI":"10.1109\/RE.2009.9"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking. In: Symbolic Model Checking, pp. 25\u201360. Springer (1993)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"31_CR21","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer Science & Business Media (2004)"},{"issue":"2","key":"31_CR22","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.J., Lerda, F.: Model checking programs. Automat. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Automat. Softw. Eng."},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Wang, Y., Guo, S., Wei Tan, C.: From code generation to software testing: AI Copilot with context-based RAG. IEEE Softw. (2025)","DOI":"10.1109\/MS.2025.3549628"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Wiesner, S., Peruzzini, M., Hauge, J.B., Thoben, K.: Requirements engineering. In: Concurrent Engineering in the 21st Century: Foundations, Developments and Challenges, pp. 103\u2013132. Springer (2015)","DOI":"10.1007\/978-3-319-13776-6_5"},{"key":"31_CR25","doi-asserted-by":"crossref","unstructured":"Zave, P., Nelson, T.: Validation of formal models: a case study. In: The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II, pp. 292\u2013313. Springer (2024)","DOI":"10.1007\/978-3-031-66673-5_15"}],"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-26220-2_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:48Z","timestamp":1783542588000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_31","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"}}]}}