{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T15:23:01Z","timestamp":1772205781918,"version":"3.50.1"},"reference-count":61,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2022,4,21]],"date-time":"2022-04-21T00:00:00Z","timestamp":1650499200000},"content-version":"am","delay-in-days":232,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/100000104","name":"NASA","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Information and Software Technology"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1016\/j.infsof.2021.106590","type":"journal-article","created":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T10:04:19Z","timestamp":1618999459000},"page":"106590","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":46,"special_numbering":"C","title":["Automated formalization of structured natural language requirements"],"prefix":"10.1016","volume":"137","author":[{"given":"Dimitra","family":"Giannakopoulou","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Pressburger","sequence":"additional","affiliation":[]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[]},{"given":"Johann","family":"Schumann","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.infsof.2021.106590_b1","series-title":"Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings","first-page":"263","article-title":"RAT: a tool for the formal analysis of requirements","volume":"Vol. 4590","author":"Bloem","year":"2007"},{"key":"10.1016\/j.infsof.2021.106590_b2","series-title":"2017 IEEE 25th International Requirements Engineering Conference (RE)","first-page":"283","article-title":"Requirements capture and analysis in assert(TM)","author":"Crapo","year":"2017"},{"key":"10.1016\/j.infsof.2021.106590_b3","series-title":"NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings","first-page":"420","article-title":"SpeAR v2.0: formalized past LTL specification and analysis of requirements","volume":"Vol. 10227","author":"Fifarek","year":"2017"},{"key":"10.1016\/j.infsof.2021.106590_b4","series-title":"NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings","first-page":"173","article-title":"Towards realizability checking of contracts using theories","volume":"Vol. 9058","author":"Gacek","year":"2015"},{"issue":"2","key":"10.1016\/j.infsof.2021.106590_b5","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","article-title":"Vacuity detection in temporal model checking","volume":"4","author":"Kupferman","year":"2003","journal-title":"Int. J. Softw. Tool. Technol. Transf."},{"key":"10.1016\/j.infsof.2021.106590_b6","series-title":"Proceedings of the 21st International Conference on Software Engineering","first-page":"411","article-title":"Patterns in property specifications for finite-state verification","author":"Dwyer","year":"1999"},{"issue":"2","key":"10.1016\/j.infsof.2021.106590_b7","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1109\/MS.2012.36","article-title":"Listen, then use EARS","volume":"29","author":"Mavin","year":"2012","journal-title":"IEEE Softw."},{"key":"10.1016\/j.infsof.2021.106590_b8","series-title":"Computer Aided Verification","first-page":"446","article-title":"The real-time graphical interval logic toolset","author":"Moser","year":"1996"},{"key":"10.1016\/j.infsof.2021.106590_b9","series-title":"CAV","first-page":"334","article-title":"The nuXmv symbolic model checker","volume":"Vol. 8559","author":"Cavada","year":"2014"},{"key":"10.1016\/j.infsof.2021.106590_b10","series-title":"TACAS","first-page":"357","article-title":"Temporal-logic based runtime observer pairs for system health management of real-time systems","author":"Reinbacher","year":"2014"},{"key":"10.1016\/j.infsof.2021.106590_b11","series-title":"Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, on, Canada, July 17-23, 2016, Proceedings, Part II","first-page":"510","article-title":"The Kind 2 model checker","author":"Champion","year":"2016"},{"key":"10.1016\/j.infsof.2021.106590_b12","series-title":"International Conference on Computer Aided Verification","first-page":"20","article-title":"The JKind model checker","author":"Gacek","year":"2018"},{"key":"10.1016\/j.infsof.2021.106590_b13","article-title":"Lectures on runtime verification","volume":"Vol. 10457","author":"Bartocci","year":"2018"},{"key":"10.1016\/j.infsof.2021.106590_b14","unstructured":"C. Elliott, 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: A.F.R. Laboratory (Ed.), Safe & Secure Systems and Software Symposium (S5), 2015."},{"key":"10.1016\/j.infsof.2021.106590_b15","unstructured":"C. Elliott, An example set of cyber-physical V&V challenges for S5, Lockheed Martin skunk works, in: A.F.R. Laboratory (Ed.), Safe & Secure Systems and Software Symposium (S5), 2016."},{"key":"10.1016\/j.infsof.2021.106590_b16","series-title":"Requirements Engineering: Foundation for Software Quality - 26th International Working Conference, REFSQ 2020, Pisa, Italy, March 24-27, 2020, Proceedings [REFSQ 2020 was postponed]","first-page":"19","article-title":"Generation of formal requirements from structured natural language","author":"Giannakopoulou","year":"2020"},{"key":"10.1016\/j.infsof.2021.106590_b17","series-title":"NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings","first-page":"13","article-title":"The theory and practice of SALT","volume":"Vol. 6617","author":"Bauer","year":"2011"},{"key":"10.1016\/j.infsof.2021.106590_b18","series-title":"Proceedings of the 27th International Conference on Software Engineering","first-page":"372","article-title":"Real-time specification patterns","author":"Konrad","year":"2005"},{"key":"10.1016\/j.infsof.2021.106590_b19","series-title":"Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020), Pisa, Italy, March 24, 2020","article-title":"Formal requirements elicitation with FRET","author":"Giannakopoulou","year":"2020"},{"key":"10.1016\/j.infsof.2021.106590_b20","series-title":"Proceedings of the 12th International Conference on Model Checking Software","first-page":"200","article-title":"Verifying pattern-generated LTL formulas: A case study","author":"Salamah","year":"2005"},{"issue":"11","key":"10.1016\/j.infsof.2021.106590_b21","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1145\/182.358434","article-title":"Maintaining knowledge about temporal intervals","volume":"26","author":"Allen","year":"1983","journal-title":"Commun. ACM"},{"key":"10.1016\/j.infsof.2021.106590_b22","series-title":"2020 IEEE 28th International Requirements Engineering Conference (RE)","first-page":"300","article-title":"The ten Lockheed Martin cyber-physical challenges: Formalized, analyzed, and explained","author":"Mavridou","year":"2020"},{"key":"10.1016\/j.infsof.2021.106590_b23","series-title":"Evaluation of the FRET and CoCoSim tools on the Ten Lockheed-Martin Cyber-Physical Challenge Problems","author":"Mavridou","year":"2019"},{"key":"10.1016\/j.infsof.2021.106590_b24","series-title":"27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE\u201919","first-page":"1015","article-title":"Evaluating model testing and model checking for finding requirements violations in Simulink models","author":"Nejati","year":"2019"},{"key":"10.1016\/j.infsof.2021.106590_b25","series-title":"Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held As Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings","first-page":"347","article-title":"CoCoSpec: A mode-aware contract language for reactive systems","author":"Champion","year":"2016"},{"issue":"9","key":"10.1016\/j.infsof.2021.106590_b26","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","article-title":"The synchronous data flow programming language LUSTRE","volume":"79","author":"Halbwachs","year":"1991","journal-title":"Proc. IEEE"},{"key":"10.1016\/j.infsof.2021.106590_b27","series-title":"Requirements Engineering Fundamentals","author":"Pohl","year":"2015"},{"key":"10.1016\/j.infsof.2021.106590_b28","series-title":"The SAREMAN project: Controlled natural language requirements in the design and analysis of safety critical I&C systems","author":"Tommila","year":"2014"},{"key":"10.1016\/j.infsof.2021.106590_b29","series-title":"Proceedings of the 2009 17th IEEE International Requirements Engineering Conference, RE","first-page":"317","article-title":"Easy approach to requirements syntax (EARS)","author":"Mavin","year":"2009"},{"key":"10.1016\/j.infsof.2021.106590_b30","series-title":"1st International Workshop on Easy Approach To Requirements Syntax (EARS)","first-page":"11","article-title":"Formalizing EARS \u2013 first impressions","author":"L\u00facio","year":"2018"},{"key":"10.1016\/j.infsof.2021.106590_b31","series-title":"NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings","first-page":"427","article-title":"Just formal enough? Automated analysis of EARS requirements","volume":"Vol. 10227","author":"L\u00facio","year":"2017"},{"key":"10.1016\/j.infsof.2021.106590_b32","series-title":"2017 IEEE 25th International Requirements Engineering Conference (RE)","first-page":"263","article-title":"A formalization method to process structured natural language to logic expressions to detect redundant specification and test statements","author":"Walter","year":"2017"},{"key":"10.1016\/j.infsof.2021.106590_b33","series-title":"VSTTE","first-page":"225","article-title":"Formalization and analysis of real-time requirements: A feasibility study at BOSCH","author":"Post","year":"2012"},{"key":"10.1016\/j.infsof.2021.106590_b34","series-title":"2019 IEEE 27th International Requirements Engineering Conference (RE)","first-page":"234","article-title":"Scalable analysis of real-time requirements","author":"Langenfeld","year":"2019"},{"key":"10.1016\/j.infsof.2021.106590_b35","unstructured":"Hanfor Documentation https:\/\/ultimate-pa.github.io\/hanfor\/ (accessed Mar 16, 2021)."},{"issue":"1","key":"10.1016\/j.infsof.2021.106590_b36","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1142\/S0218194004001567","article-title":"Supporting elicitation and specification of software properties through patterns and composite propositions","volume":"14","author":"Mondragon","year":"2004","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"10.1016\/j.infsof.2021.106590_b37","doi-asserted-by":"crossref","DOI":"10.1155\/2011\/869182","article-title":"Towards support for software model checking: Improving the efficiency of formal specifications","volume":"2011","author":"Salamah","year":"2011","journal-title":"Adv. Softw. Eng."},{"issue":"8","key":"10.1016\/j.infsof.2021.106590_b38","doi-asserted-by":"crossref","first-page":"1915","DOI":"10.1016\/j.jss.2012.02.041","article-title":"Validated templates for specification of complex LTL formulas","volume":"85","author":"Salamah","year":"2012","journal-title":"J. Syst. Softw."},{"key":"10.1016\/j.infsof.2021.106590_b39","series-title":"Proceedings of the 24th International Conference on Software Engineering","first-page":"11","article-title":"PROPEL: An approach supporting property elucidation","author":"Smith","year":"2002"},{"key":"10.1016\/j.infsof.2021.106590_b40","series-title":"Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering","first-page":"208","article-title":"User guidance for creating precise and accessible property specifications","author":"Cobleigh","year":"2006"},{"key":"10.1016\/j.infsof.2021.106590_b41","series-title":"34th Formal Techniques for Networked and Distributed Systems (FORTE)","first-page":"17","article-title":"Property specification made easy: Harnessing the power of model checking in UML designs","author":"Remenska","year":"2014"},{"key":"10.1016\/j.infsof.2021.106590_b42","series-title":"2019 IEEE 27th International Requirements Engineering Conference Workshops (REW)","first-page":"123","article-title":"Formal requirements and constraints modelling in FORM-l for the engineering of complex socio-technical systems","author":"Nguyen","year":"2019"},{"key":"10.1016\/j.infsof.2021.106590_b43","doi-asserted-by":"crossref","unstructured":"D. Bouskela, A. Jardin, ETL: A new temporal language for the verification of cyber-physical systems, in: 2018 Annual IEEE International Systems Conference (SysCon), 2018, pp. 1\u20138.","DOI":"10.1109\/SYSCON.2018.8369502"},{"key":"10.1016\/j.infsof.2021.106590_b44","series-title":"2017 IEEE\/AIAA 36th Digital Avionics Systems Conference (DASC)","first-page":"1","article-title":"Flight critical software and systems development using ASSERT\u2122","author":"Siu","year":"2017"},{"key":"10.1016\/j.infsof.2021.106590_b45","series-title":"8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France","article-title":"Debugging embedded systems requirements with STIMULUS: an automotive case-study","author":"Jeannet","year":"2016"},{"key":"10.1016\/j.infsof.2021.106590_b46","series-title":"19th GI\/ITG\/GMM Workshop Methoden Und Beschreibungssprachen Zur Modellierung Und Verifikation Von Schaltungen Und Systemen, MBMV 2016, Freiburg Im Breisgau, Germany, March 1-2, 2016","first-page":"6","article-title":"Universal pattern: Formalization, testing, coverage, verification, and test case generation for safety-critical requirements","author":"Teige","year":"2016"},{"key":"10.1016\/j.infsof.2021.106590_b47","series-title":"2019 IEEE 17th International Conference on Industrial Informatics (INDIN), Vol. 1","first-page":"400","article-title":"Formalization of natural language requirements into temporal logics: a survey","author":"Buzhinsky","year":"2019"},{"key":"10.1016\/j.infsof.2021.106590_b48","series-title":"2014 IEEE 22nd International Requirements Engineering Conference (RE)","first-page":"325","article-title":"VARED: Verification and analysis of requirements and early designs","author":"Badger","year":"2014"},{"key":"10.1016\/j.infsof.2021.106590_b49","series-title":"NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings","first-page":"41","article-title":"ARSENAL: automatic requirements specification extraction from natural language","volume":"Vol. 9690","author":"Ghosh","year":"2016"},{"key":"10.1016\/j.infsof.2021.106590_b50","series-title":"LFM 2000: Fifth NASA Langley Formal Methods Workshop","first-page":"187","article-title":"An overview of SAL","author":"Bensalem","year":"2000"},{"key":"10.1016\/j.infsof.2021.106590_b51","unstructured":"D. Elenius, E. Yeh, S. Graham-Lengrand, S. Ghosh, P. Lincoln, N. Shankar, Deriving formal specifications from natural language requirements using ARSENAL2, in: High Confidence Software and Systems Conference, 2019."},{"issue":"10","key":"10.1016\/j.infsof.2021.106590_b52","doi-asserted-by":"crossref","first-page":"944","DOI":"10.1109\/TSE.2015.2428709","article-title":"Automated checking of conformance to requirements templates using natural language processing","volume":"41","author":"Arora","year":"2015","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.infsof.2021.106590_b53","series-title":"IBM Requirements Quality Assistant","year":"2021"},{"key":"10.1016\/j.infsof.2021.106590_b54","series-title":"QRA QVscribe","year":"2021"},{"key":"10.1016\/j.infsof.2021.106590_b55","series-title":"Guide for Writing Requirements","author":"INCOSE","year":"2019"},{"key":"10.1016\/j.infsof.2021.106590_b56","series-title":"Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020), Pisa, Italy, March 24, 2020","article-title":"Bridging the gap between requirements and Simulink model analysis","author":"Mavridou","year":"2020"},{"key":"10.1016\/j.infsof.2021.106590_b57","series-title":"10th European Congress on Embedded Real Time Software and Systems (ERTS 2020)","article-title":"CoCoSim, a code generation framework for control\/command applications: An overview of cocosim for multi-periodic discrete Simulink models","author":"Bourbouh","year":"2020"},{"key":"10.1016\/j.infsof.2021.106590_b58","series-title":"Rapid prototyping in PVS","author":"Mu\u00f1oz","year":"2003"},{"key":"10.1016\/j.infsof.2021.106590_b59","doi-asserted-by":"crossref","unstructured":"H. Bourbouh, M. Farrell, A. Mavridou, I. Sljivo, G. Brat, L.A. Dennis, M. Fisher, Integrating formal verification and assurance: an inspection rover case study, in: NASA Formal Methods - 13th International Symposium, NFM 2021, May 24-28, 2021, Proceedings, 2021.","DOI":"10.1007\/978-3-030-76384-8_4"},{"key":"10.1016\/j.infsof.2021.106590_b60","series-title":"Integration and evaluation of the AdvoCATE, FRET, CoCoSim, and Event-B tools on the Inspection Rover Case Study","author":"Bourbouh","year":"2021"},{"key":"10.1016\/j.infsof.2021.106590_b61","doi-asserted-by":"crossref","unstructured":"A. Dutle, C. Munoz, E. Conrad, A. Goodloe, L. Titolo, I. Perez, S. Balachandran, D. Giannakopoulou, A. Mavridou, T. Pressburger, From requirements to autonomous flight: an overview of the monitoring ICAROUS project, in: Second Workshop on Formal Methods for Autonomous Systems, 2020.","DOI":"10.4204\/EPTCS.329.3"}],"container-title":["Information and Software Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0950584921000707?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0950584921000707?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:32:16Z","timestamp":1760585536000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0950584921000707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9]]},"references-count":61,"alternative-id":["S0950584921000707"],"URL":"https:\/\/doi.org\/10.1016\/j.infsof.2021.106590","relation":{},"ISSN":["0950-5849"],"issn-type":[{"value":"0950-5849","type":"print"}],"subject":[],"published":{"date-parts":[[2021,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Automated formalization of structured natural language requirements","name":"articletitle","label":"Article Title"},{"value":"Information and Software Technology","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.infsof.2021.106590","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"106590"}}