{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:18Z","timestamp":1783545318313,"version":"3.55.0"},"publisher-location":"Cham","reference-count":38,"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                    Formal methods enable the verification of system behavior against requirements that are expressed as formal, mathematical properties. However, translating the often ambiguous natural language requirements that are typically produced by developers and engineers into precise mathematical specifications remains a significant bottleneck in the formal verification process. NASA\u2019s Formal Requirements Elicitation Tool (\n                    <jats:sc>FRET<\/jats:sc>\n                    ) is an open source tool that addresses this challenge by bridging the gap between natural language requirements and formal specifications that are suitable for automated verification.\n                    <jats:sc>FRET<\/jats:sc>\n                    enables practitioners to express requirements in\n                    <jats:sc>FRETish<\/jats:sc>\n                    , a structured natural language, that balances intuitive readability with formal rigor.\n                    <jats:sc>FRET<\/jats:sc>\n                    automatically translates these requirements into formal properties that verification tools can directly process. This tutorial paper introduces FRET and guides readers through expressing requirements in\n                    <jats:sc>FRETish<\/jats:sc>\n                    . We present the tool\u2019s key analysis capabilities, including simulation, realizability checking, test-case generation, and automated generation of verification conditions for external formal verification tools. Our goal is to provide a comprehensive guide that helps practitioners, regardless of their formal methods background, to effectively leverage\n                    <jats:sc>FRET<\/jats:sc>\n                    in their verification and validation (V&amp;V) workflows.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_21","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:19:48Z","timestamp":1779023988000},"page":"420-445","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Requirements Elicitation, Formalization, and\u00a0Analysis with\u00a0FRET: A Tutorial"],"prefix":"10.1007","author":[{"given":"Anastasia","family":"Mavridou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Katis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mari A.","family":"Aoki","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marie","family":"Farrell","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1d\u00e1m, Z., et al.: From natural language requirements to the verification of programmable logic controllers: integrating FRET into PLCverif. In: NASA Formal Methods, pp. 353\u2013360. Springer (2023)","DOI":"10.1007\/978-3-031-33170-1_21"},{"key":"21_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Cavada, R., et\u00a0al.: The nuXmv symbolic model checker. In: International Conference on Computer Aided Verification, pp. 334\u2013342. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-41591-8_24","volume-title":"Software Engineering and Formal Methods","author":"A Champion","year":"2016","unstructured":"Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 347\u2013366. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_24"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Champion, A., ebsout, 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":"21_CR6","doi-asserted-by":"crossref","unstructured":"Cheng, B.H., Atlee, J.M.: Research directions in requirements engineering. In: Future of Software Engineering, pp. 285\u2013303. IEEE (2007)","DOI":"10.1109\/FOSE.2007.17"},{"key":"21_CR7","unstructured":"Chung, L., Nixon, B.A., Yu, E., Mylopoulos, J.: Non-Functional requirements in software engineering, vol. 5. Springer (2012)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., et\u00a0al.: NuSMV Version 2: an opensource tool for symbolic model checking. In: International Conference on Computer-Aided Verification. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"21_CR9","unstructured":"Darvas, D., Vinuela, E.B., Adiego, E.F.: PLCverif: A tool to verify PLC programs based on model checking techniques. In: International Conference on Accelerator and Large Experimental Physics Control Systems. JACoW (2015)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"De\u00a0Ferro, C.M., Mavridou, A., Dille, M., Martins, F.: Simplifying requirements formalization for resource-constrained mission-critical software. In: International Conference on Dependable Systems and Networks Workshops, pp. 263\u2013266 (2023)","DOI":"10.1109\/DSN-W58399.2023.00066"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"21_CR12","unstructured":"Elliott, C.: On example models and challenges ahead for the evaluation of complex cyber-physical systems with state of the art formal methods V&V, Lockheed Martin Skunk works. In: Safe & Secure Systems and Software Symposium, pp. 9\u201311 (2015)"},{"key":"21_CR13","unstructured":"Elliott, C.: An example set of cyber-physical V&V challenges for S5, Lockheed Martin Skunk Works. In: Safe & Secure Systems and Software Symposium, pp. 12\u201314 (2016)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Farrell, M., Luckcuck, M., Monahan, R., Reynolds, C., Sheridan, O.: Adventures in FRET and specification. In: International Symposium on Leveraging Applications of Formal Methods, pp. 106\u2013123. Springer (2024)","DOI":"10.1007\/978-3-031-75380-0_7"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R.: Towards refactoring FRETish requirements. In: NASA Formal Methods Symposium, pp. 272\u2013279. Springer (2022)","DOI":"10.1007\/978-3-031-06773-0_14"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Fink, X., Mavridou, A., Katis, A., Adiego, B.F.: Verifying PLC programs via monitors: extending the Integration of FRET and PLCverif. In: NASA Formal Methods, pp. 427\u2013435. Springer (2024)","DOI":"10.1007\/978-3-031-60698-4_26"},{"key":"21_CR17","unstructured":"Giannakopoulou, D., et\u00a0al.: Formal requirements elicitation with FRET. In: Requirements Engineering: Foundation for Software Quality, p. 1 (2020)"},{"key":"21_CR18","doi-asserted-by":"publisher","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":"21_CR19","doi-asserted-by":"crossref","unstructured":"Katis, A., et\u00a0al.: Validity-Guided synthesis of reactive systems from assume-guarantee contracts. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 176\u2013193. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_10"},{"key":"21_CR20","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":"21_CR21","doi-asserted-by":"crossref","unstructured":"Katis, A., Mavridou, A., Pressburger, T.: A streamlined, formal approach to requirements-based testing. In: NASA Formal Methods, pp. 159\u2013179. Springer (2025)","DOI":"10.1007\/978-3-031-93706-4_10"},{"key":"21_CR22","volume-title":"Mu-FRET: a catalogue and tool for requirement refactoring","author":"M Luckcuck","year":"2026","unstructured":"Luckcuck, M., Sheridan, O., Farrell, M., Monahan, R.: Mu-FRET: a catalogue and tool for requirement refactoring. Software and Systems Modeling, To Appear (2026)"},{"key":"21_CR23","unstructured":"Malan, R., Bredemeyer, D.: Functional requirements and use cases. Bredemeyer Consulting, pp. 335\u20131653 (2001)"},{"key":"21_CR24","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.infsof.2016.04.002","volume":"75","author":"LEG Martins","year":"2016","unstructured":"Martins, L.E.G., Gorschek, T.: Requirements engineering for safety-critical systems: a systematic literature review. Inf. Softw. Technol. 75, 71\u201389 (2016)","journal-title":"Inf. Softw. Technol."},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Mavridou, A., et\u00a0al.: The Ten Lockheed martin cyber-physical challenges: formalized, analyzed, and explained. In: International Requirements Engineering Conference, pp. 300\u2013310. IEEE (2020)","DOI":"10.1109\/RE48521.2020.00040"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-030-90870-6_27","volume-title":"Formal Methods","author":"A Mavridou","year":"2021","unstructured":"Mavridou, A., Katis, A., Giannakopoulou, D., Kooi, D., Pressburger, T., Whalen, M.W.: From partial to global assume-guarantee contracts: compositional realizability analysis in FRET. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 503\u2013523. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_27"},{"key":"21_CR27","unstructured":"Mendoza, D., Mavridou, A., Katis, A., Trippel, C.: Automating requirements formalization: using LLMs and low-complexity distinguishing traces for semantic validation. In: IEEE\/ACM International Conference on Software Engineering (2026)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Mirani, M., Inverardi, P., Pelliccione, P., Raimondi, F., Troquard, N.: Extending FRET with SLEEC Rules: formalization, obligation inference, and monitoring. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, To appear (2026)","DOI":"10.1007\/978-3-032-22749-2_4"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Pecheur, C., Raimondi, F., Brat, G.: A formal analysis of requirements-based testing. In: International Symposium on Software Testing and Analysis, pp. 47\u201356. ACM (2009)","DOI":"10.1145\/1572272.1572279"},{"key":"21_CR30","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: Tools and Algorithms for the Construction and Analysis of Systems, pp. 387\u2013395. Springer, 2022","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"21_CR31","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: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 387\u2013395. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Perez, I., Mavridou, A., Pressburger, T., Will, A., Martin, P.J.: Monitoring ROS2: from requirements to autonomous robots. In: International Workshop on Formal Methods for Autonomous Systems (2022)","DOI":"10.4204\/EPTCS.371.15"},{"key":"21_CR33","volume-title":"Requirements Engineering: An Overview","author":"K Pohl","year":"1996","unstructured":"Pohl, K.: Requirements Engineering: An Overview. RWTH, Fachgruppe Informatik Aachen (1996)"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Pressburger, T., Katis, A., Dutle, A., Mavridou, A.: Authoring, analyzing, and monitoring requirements for a Lift-Plus-Cruise aircraft. In: Requirements Engineering: Foundation for Software Quality, pp. 295\u2013308. Springer (2023)","DOI":"10.1007\/978-3-031-29786-1_21"},{"key":"21_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-48869-1_2","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"KY Rozier","year":"2016","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 8\u201326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2"},{"key":"21_CR36","unstructured":"Rozier, K.Y., Schumann, J.: R2U2: tool overview. In: International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, number ARC-E-DAA-TN48849 (2017)"},{"key":"21_CR37","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.jss.2018.07.053","volume":"145","author":"E Stachtiari","year":"2018","unstructured":"Stachtiari, E., Mavridou, A., Katsaros, P., Bliudze, S., Sifakis, J.: Early validation of system requirements and design through correctness-by-construction. J. Syst. Softw. 145, 52\u201378 (2018)","journal-title":"J. Syst. Softw."},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Van\u00a0Lamsweerde, A.: Requirements engineering in the year 00: a research Perspective. In: International Conference on Software Engineering, pp. 5\u201319 (2000)","DOI":"10.1145\/337180.337184"}],"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_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:10Z","timestamp":1783542550000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_21","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"}}]}}