{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:12Z","timestamp":1781238912111,"version":"3.54.1"},"publisher-location":"Cham","reference-count":37,"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_22","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:38Z","timestamp":1749316958000},"page":"380-399","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["TRACE: Toolkit for\u00a0Requirements Analysis, Capture, and\u00a0Elicitation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4620-4266","authenticated-orcid":false,"given":"Sarat Chandra","family":"Varanasi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3284-1969","authenticated-orcid":false,"given":"Baoluo","family":"Meng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9242-019X","authenticated-orcid":false,"given":"Robert","family":"Lorch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7027-2082","authenticated-orcid":false,"given":"Abha","family":"Moitra","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5232-1098","authenticated-orcid":false,"given":"Kit","family":"Siu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1792-9858","authenticated-orcid":false,"given":"Saswata","family":"Paul","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6660-2667","authenticated-orcid":false,"given":"Michael","family":"Durling","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4476-0135","authenticated-orcid":false,"given":"Neha","family":"Beniwal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikita","family":"Visnevski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et\u00a0al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Ro\u010dkai, P.: DiVinE: parallel distributed model checker. In: 2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology, pp.\u00a04\u20137. IEEE (2010). https:\/\/doi.org\/10.1109\/PDMC-HiBi.2010.9","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"key":"22_CR3","unstructured":"Bhatt, D., Murugesan, A., Hall, B., Ren, H., Jeppu, Y.: The CLEAR way to transparent formal methods. In: 4th Workshop on Formal Integrated Development Environment (2018)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2010","unstructured":"Bloem, R., et al.: RATSY \u2013 a new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425\u2013429. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_37"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"A Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652\u2013657. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-19835-9_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HR Chamarthi","year":"2011","unstructured":"Chamarthi, H.R., Dillinger, P., Manolios, P., Vroon, D.: The ACL2 sedan theorem proving system. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 291\u2013295. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_27"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 510\u2013517. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-662-54577-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C-H Cheng","year":"2017","unstructured":"Cheng, C.-H., Lee, E.A., Ruess, H.: autoCode4: structural controller synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part I. LNCS, vol. 10205, pp. 398\u2013404. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_23"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Crapo, A., Moitra, A., McMillan, C., Russell, D.: Requirements capture and analysis in ASSERTTM. In: 2017 IEEE 25th International Requirements Engineering Conference (RE), pp. 283\u2013291. IEEE (2017). https:\/\/doi.org\/10.1109\/RE.2017.54","DOI":"10.1109\/RE.2017.54"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2004","unstructured":"de Moura, L., et al.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496\u2013500. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_45"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Delligatti, L.: SysML Distilled: A Brief Guide to the Systems Modeling Language. Addison-Wesley (2013). https:\/\/doi.org\/10.5555\/2560076","DOI":"10.5555\/2560076"},{"key":"22_CR13","unstructured":"Elenius, D., Yeh, E., Graham-Lengrand, S., Ghosh, S., Lincoln, P., Shankar, N.: Deriving formal specifications from natural language requirements using arsenal 2. In: High Confidence Software and Systems Conference (2019)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-319-57288-8_30","volume-title":"NASA Formal Methods","author":"AW Fifarek","year":"2017","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: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 420\u2013426. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_30"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Filippidis, I., Dathathri, S., Livingston, S.C., Ozay, N., Murray, R.M.: Control design for hybrid systems with TuLiP: the temporal logic planning toolbox. In: 2016 IEEE Conference on Control Applications (CCA), pp. 1030\u20131041. IEEE (2016). https:\/\/doi.org\/10.1109\/CCA.2016.7587949","DOI":"10.1109\/CCA.2016.7587949"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-96142-2_3","volume-title":"Computer Aided Verification","author":"A Gacek","year":"2018","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, L., Ghassabani, E.: The JKind model checker. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 20\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-17524-9_13","volume-title":"NASA Formal Methods","author":"A Gacek","year":"2015","unstructured":"Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.: Towards realizability checking of contracts using theories. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 173\u2013187. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_13"},{"key":"22_CR18","unstructured":"Gallegos, I., Ochoa, O., Gates, A.Q., Roach, S., Salamah, S., Vela, C.: A property specification tool for generating formal specifications: Prospec 2.0. In: SEKE, pp. 273\u2013278 (2008)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-319-40648-0_4","volume-title":"NASA Formal Methods","author":"S Ghosh","year":"2016","unstructured":"Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W.: ARSENAL: automatic requirements specification extraction from natural language. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 41\u201346. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_4"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Gross, K.H., Fifarek, A.W., Hoffman, J.A.: Incremental formal methods based design approach demonstrated on a coupled tanks control system. In: 2016 IEEE 17th International Symposium on High Assurance Systems Engineering (HASE), pp. 181\u2013188. IEEE (2016). https:\/\/doi.org\/10.1109\/HASE.2016.16","DOI":"10.1109\/HASE.2016.16"},{"issue":"5","key":"22_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans. Software Eng."},{"key":"22_CR22","doi-asserted-by":"publisher","DOI":"10.1145\/3704736","author":"I Incer","year":"2024","unstructured":"Incer, I., Badithela, A., Graebener, J.B., Mallozzi, P., Pandey, A., Rouquette, N., Yu, S.J., Benveniste, A., Caillaud, B., Murray, R.M., et al.: Pacti: assume-guarantee contracts for efficient compositional analysis and design. ACM Trans. Cyber-Phys. Syst. (2024). https:\/\/doi.org\/10.1145\/3704736","journal-title":"ACM Trans. Cyber-Phys. Syst."},{"issue":"5","key":"22_CR23","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1108\/AEAT-05-2019-0098","volume":"92","author":"RH Jansen","year":"2020","unstructured":"Jansen, R.H., Bowman, C.L., Clarke, S., Avanesian, D., Dempsey, P.J., Dyson, R.W.: NASA electrified aircraft propulsion efforts. Aircr. Eng. Aerosp. Technol. 92(5), 667\u2013673 (2020). https:\/\/doi.org\/10.1108\/AEAT-05-2019-0098","journal-title":"Aircr. Eng. Aerosp. Technol."},{"key":"22_CR24","unstructured":"Jeannet, B., Gaucher, F.: Debugging embedded systems requirements with stimulus: an automotive case-study. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016) (2016)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258\u2013262. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_29"},{"key":"22_CR26","doi-asserted-by":"publisher","unstructured":"Katis, A., Mavridou, A., Giannakopoulou, D., Pressburger, T., Schumann, J.: Capture, analyze, diagnose: realizability checking of requirements in FRET. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part II. LNCS, vol. 13372, pp. 490\u2013504. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_24","DOI":"10.1007\/978-3-031-13188-2_24"},{"key":"22_CR27","doi-asserted-by":"publisher","unstructured":"Kaufmann, M., Moore, J.S.: ACL2: An industrial strength version of Nqthm. In: Proceedings of 11th Annual Conference on Computer Assurance, COMPASS 1996, pp. 23\u201334. IEEE (1996). https:\/\/doi.org\/10.1109\/CMPASS.1996.507872","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"22_CR28","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1109\/DASC43569.2019.9081726","DOI":"10.1109\/DASC43569.2019.9081726"},{"key":"22_CR29","doi-asserted-by":"publisher","unstructured":"Lorch, R., et al.: Formal methods in requirements engineering: survey and future directions. In: International Conference on Formal Methods in Software Engineering (FormaliSE 2024) (2024). https:\/\/doi.org\/10.1145\/3644033.3644373","DOI":"10.1145\/3644033.3644373"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-319-57288-8_31","volume-title":"NASA Formal Methods","author":"L L\u00facio","year":"2017","unstructured":"L\u00facio, L., Rahman, S., Cheng, C.-H., Mavin, A.: Just formal enough? Automated analysis of EARS requirements. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 427\u2013434. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_31"},{"issue":"5","key":"22_CR31","doi-asserted-by":"publisher","first-page":"1553","DOI":"10.1007\/s10270-021-00868-z","volume":"20","author":"S Maoz","year":"2021","unstructured":"Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw. Syst. Model. 20(5), 1553\u20131586 (2021). https:\/\/doi.org\/10.1007\/s10270-021-00868-z","journal-title":"Softw. Syst. Model."},{"key":"22_CR32","unstructured":"MathWorks, Inc.: Mathworks Simulink. https:\/\/www.mathworks.com\/products\/simulink.html"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"22_CR34","doi-asserted-by":"publisher","unstructured":"Nuzzo, P., Lora, M., Feldman, Y.A., Sangiovanni-Vincentelli, A.L.: CHASE: contract-based requirement engineering for cyber-physical system design. In: 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 839\u2013844. IEEE (2018). https:\/\/doi.org\/10.23919\/DATE.2018.8342122","DOI":"10.23919\/DATE.2018.8342122"},{"key":"22_CR35","unstructured":"Somenzi, F.: CUDD: CU decision diagram package-release 2.4. 0. Univ. Colorado Boulder 21 (2009)"},{"issue":"1","key":"22_CR36","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/3379106.3379110","volume":"39","author":"L Wagner","year":"2020","unstructured":"Wagner, L.: Formal specification and analysis of requirements using SpeAR. ACM SIGAda Ada Lett. 39(1), 20\u201334 (2020). https:\/\/doi.org\/10.1145\/3379106.3379110","journal-title":"ACM SIGAda Ada Lett."},{"issue":"6","key":"22_CR37","doi-asserted-by":"publisher","first-page":"1115","DOI":"10.1109\/JPROC.2021.3073291","volume":"109","author":"P Wheeler","year":"2021","unstructured":"Wheeler, P., Sirimanna, T.S., Bozhko, S., Haran, K.S.: Electric\/hybrid-electric aircraft propulsion systems. Proc. IEEE 109(6), 1115\u20131127 (2021). https:\/\/doi.org\/10.1109\/JPROC.2021.3073291","journal-title":"Proc. IEEE"}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:41Z","timestamp":1749316961000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_22","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"}}]}}