{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T16:16:06Z","timestamp":1778256966557,"version":"3.51.4"},"reference-count":138,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2021,5,25]],"date-time":"2021-05-25T00:00:00Z","timestamp":1621900800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Ministry of Digital Development, Communications and Mass Media of the Russian Federation and Russian Venture Company","award":["004\/20 dd. 20.03.2020 and IGK 0000000007119P190002"],"award-info":[{"award-number":["004\/20 dd. 20.03.2020 and IGK 0000000007119P190002"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2022,6,30]]},"abstract":"<jats:p>A major determinant of the quality of software systems is the quality of their requirements, which should be both understandable and precise. Most requirements are written in natural language, which is good for understandability but lacks precision.<\/jats:p>\n          <jats:p>To make requirements precise, researchers have for years advocated the use of mathematics-based notations and methods, known as \u201cformal.\u201d Many exist, differing in their style, scope, and applicability. The present survey discusses some of the main formal approaches and compares them to informal methods.<\/jats:p>\n          <jats:p>The analysis uses a set of nine complementary criteria, such as level of abstraction, tool availability, and traceability support. It classifies the approaches into five categories based on their principal style for specifying requirements: natural-language, semi-formal, automata\/graphs, mathematical, and seamless (programming-language-based). It includes examples from all of these categories, altogether 21 different approaches, including for example SysML, Relax, Eiffel, Event-B, and Alloy.<\/jats:p>\n          <jats:p>The review discusses a number of open questions, including seamlessness, the role of tools and education, and how to make industrial applications benefit more from the contributions of formal approaches.<\/jats:p>","DOI":"10.1145\/3448975","type":"journal-article","created":{"date-parts":[[2021,5,25]],"date-time":"2021-05-25T13:02:30Z","timestamp":1621947750000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["The Role of Formalism in System Requirements"],"prefix":"10.1145","volume":"54","author":[{"given":"Jean-Michel","family":"Bruel","sequence":"first","affiliation":[{"name":"University of Toulouse, IRIT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sophie","family":"Ebersold","sequence":"additional","affiliation":[{"name":"University of Toulouse, IRIT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Galinier","sequence":"additional","affiliation":[{"name":"University of Toulouse, IRIT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Mazzara","sequence":"additional","affiliation":[{"name":"Innopolis University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7683-0751","authenticated-orcid":false,"given":"Alexandr","family":"Naumchev","sequence":"additional","affiliation":[{"name":"Innopolis University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[{"name":"Schaffhausen Institute of Technology and Innopolis University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,5,25]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial J. R.","unstructured":"J. R. Abrial . 2010. Modeling in Event-B: System and Software Engineering . Cambridge University Press . J. R. Abrial. 2010. Modeling in Event-B: System and Software Engineering. Cambridge University Press."},{"key":"e_1_2_1_2_1","unstructured":"J. R. Abrial S. A. Schuman and B. Meyer. 1980. Specification language. In On the Construction of Programs. Cambridge University Press 343--410.  J. R. Abrial S. A. Schuman and B. Meyer. 1980. Specification language. In On the Construction of Programs. Cambridge University Press 343--410."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"S. Abualhaija C. Arora M. Sabetzadeh L. C. Briand and E. Vaz. 2019. A machine learning-based approach for demarcating requirements in textual specifications. In RE. IEEE 51--62.  S. Abualhaija C. Arora M. Sabetzadeh L. C. Briand and E. Vaz. 2019. A machine learning-based approach for demarcating requirements in textual specifications. In RE. IEEE 51--62.","DOI":"10.1109\/RE.2019.00017"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"D. Aceituna H. Do G. Singh Walia and S. W. Lee. 2011. Evaluating the use of model-based requirements verification method: A feasibility study. In EmpiRE. IEEE Computer Society 13--20.  D. Aceituna H. Do G. Singh Walia and S. W. Lee. 2011. Evaluating the use of model-based requirements verification method: A feasibility study. In EmpiRE. IEEE Computer Society 13--20.","DOI":"10.1109\/EmpiRE.2011.6046248"},{"key":"e_1_2_1_5_1","volume-title":"TFM, Lecture Notes in Computer Science","author":"Aceto L.","unstructured":"L. Aceto , A. Ing\u00f3lfsd\u00f3ttir , K. Guldstrand Larsen , and J.\u00ed Srba. 2009. Teaching concurrency: Theory in practice . In TFM, Lecture Notes in Computer Science , Vol. 5846 . Springer , 158--175. L. Aceto, A. Ing\u00f3lfsd\u00f3ttir, K. Guldstrand Larsen, and J.\u00ed Srba. 2009. Teaching concurrency: Theory in practice. In TFM, Lecture Notes in Computer Science, Vol. 5846. Springer, 158--175."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(03)00244-5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0394-x"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207390903372429"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2428709"},{"key":"e_1_2_1_10_1","volume-title":"OWL: Web ontology language. In Encyclopedia of Database Systems","author":"Bechhofer S.","year":"2018","unstructured":"S. Bechhofer . 2018 . OWL: Web ontology language. In Encyclopedia of Database Systems ( 2 nd ed.). Springer . S. Bechhofer. 2018. OWL: Web ontology language. In Encyclopedia of Database Systems (2nd ed.). Springer.","edition":"2"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"B. Berenbach F. Schneider and H. Naughton. 2012. The use of a requirements modeling language for industrial applications. In RE. IEEE Computer Society 285--290.  B. Berenbach F. Schneider and H. Naughton. 2012. The use of a requirements modeling language for industrial applications. In RE. IEEE Computer Society 285--290.","DOI":"10.1109\/RE.2012.6345816"},{"key":"e_1_2_1_12_1","volume-title":"Lecture Notes in Computer Science","volume":"61","author":"Bj\u00f8rner D.","year":"1978","unstructured":"D. Bj\u00f8rner and C. B. Jones ( Eds .). 1978 . The Vienna Development Method: The Meta-Language . Lecture Notes in Computer Science , Vol. 61 . Springer. D. Bj\u00f8rner and C. B. Jones (Eds.). 1978. The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, Vol. 61. Springer."},{"key":"e_1_2_1_13_1","volume-title":"Communications in Computer and Information Science","volume":"433","author":"Boniol F.","unstructured":"F. Boniol and V. Wiels . 2014. The landing gear system case study. In ABZ (Case Study) , Communications in Computer and Information Science , Vol. 433 . Springer, 1--18. F. Boniol and V. Wiels. 2014. The landing gear system case study. In ABZ (Case Study), Communications in Computer and Information Science, Vol. 433. Springer, 1--18."},{"key":"e_1_2_1_14_1","unstructured":"P. Bourque and Richard E. Fairley (Eds.). 2014. Guide to the Software Engineering Body of Knowledge (SWEBOK(R)): Version 3.0 (3rd ed.). IEEE Computer Society Press.  P. Bourque and Richard E. Fairley (Eds.). 2014. Guide to the Software Engineering Body of Knowledge (SWEBOK(R)): Version 3.0 (3rd ed.). IEEE Computer Society Press."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-017-0619-4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"J. M. Bruel S. Ebersold F. Galinier A. Naumchev M. Mazzara and B. Meyer. 2021. The role of formalism in system requirements (additional material). https:\/\/github.com\/anaumchev\/requirements_survey\/blob\/main\/The_role_of_formalism_in_system_requirements___additional_material_.pdf.  J. M. Bruel S. Ebersold F. Galinier A. Naumchev M. Mazzara and B. Meyer. 2021. The role of formalism in system requirements (additional material). https:\/\/github.com\/anaumchev\/requirements_survey\/blob\/main\/The_role_of_formalism_in_system_requirements___additional_material_.pdf.","DOI":"10.1145\/3448975"},{"key":"e_1_2_1_17_1","unstructured":"Capterra. 2015. Retrieved from https:\/\/www.capterra.com\/requirements-management-software\/.  Capterra. 2015. Retrieved from https:\/\/www.capterra.com\/requirements-management-software\/."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.81"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"N.\n      Cata\u00f1o\n     and \n      C.\n      Rueda\n  . \n  2009\n  . Teaching formal methods for the unconquered territory. In TFM Lecture Notes in Computer Science Vol. \n  5846\n  . \n  Springer 2--19.  N. Cata\u00f1o and C. Rueda. 2009. Teaching formal methods for the unconquered territory. In TFM Lecture Notes in Computer Science Vol. 5846. Springer 2--19.","DOI":"10.1007\/978-3-642-04912-5_2"},{"key":"e_1_2_1_20_1","volume-title":"Continuous System Modeling","author":"Cellier F. E.","unstructured":"F. E. Cellier . 1991. Continuous System Modeling . Springer . F. E. Cellier. 1991. Continuous System Modeling. Springer."},{"key":"e_1_2_1_21_1","volume-title":"Software Pioneers","author":"Chen P. Pin-Shan","unstructured":"P. Pin-Shan Chen . 2002. The entity relationship model - Toward a unified view of data (reprint) . In Software Pioneers . Springer , Berlin , 311--339. P. Pin-Shan Chen. 2002. The entity relationship model - Toward a unified view of data (reprint). In Software Pioneers. Springer, Berlin, 311--339."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/357980.358007"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"J. L. Cola\u00e7o B. Pagano and M. Pouzet. 2005. A conservative extension of synchronous data-flow with state machines. In EMSOFT. ACM 173--182.  J. L. Cola\u00e7o B. Pagano and M. Pouzet. 2005. A conservative extension of synchronous data-flow with state machines. In EMSOFT. ACM 173--182.","DOI":"10.1145\/1086228.1086261"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"A.\n      Cuccuru C.\n      Mraidha F.\n      Terrier and \n      S.\n      G\u00e9rard\n  . \n  2007\n  . Enhancing UML extensions with operational semantics. In MoDELS Lecture Notes in Computer Science Vol. \n  4735\n  . \n  Springer 271--285.  A. Cuccuru C. Mraidha F. Terrier and S. G\u00e9rard. 2007. Enhancing UML extensions with operational semantics. In MoDELS Lecture Notes in Computer Science Vol. 4735. Springer 271--285.","DOI":"10.1007\/978-3-540-75209-7_19"},{"key":"e_1_2_1_25_1","first-page":"1","article-title":"Empirical evaluation of formal method for requirements specification in agile approaches","volume":"53","author":"Rodrigues P. L.","year":"2018","unstructured":"P. L. da R. Rodrigues , M. Ecar , S. V. Menezes , J. P. S. da Silva , G. T. A. Guedes , and E. de M. Rodrigues . 2018 . Empirical evaluation of formal method for requirements specification in agile approaches . In SBSI. ACM , 53 : 1 -- 53 :8. P. L. da R. Rodrigues, M. Ecar, S. V. Menezes, J. P. S. da Silva, G. T. A. Guedes, and E. de M. Rodrigues. 2018. Empirical evaluation of formal method for requirements specification in agile approaches. In SBSI. ACM, 53:1--53:8.","journal-title":"SBSI. ACM"},{"key":"e_1_2_1_26_1","volume-title":"Teaching goal modeling in undergraduate education. In iStarT@CAiSE (CEUR Workshop Proceedings)","author":"Dalpiaz F.","unstructured":"F. Dalpiaz . 2015. Teaching goal modeling in undergraduate education. In iStarT@CAiSE (CEUR Workshop Proceedings) , Vol. 1370 . CEUR-WS. org, 1--6. F. Dalpiaz. 2015. Teaching goal modeling in undergraduate education. In iStarT@CAiSE (CEUR Workshop Proceedings), Vol. 1370. CEUR-WS.org, 1--6."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(93)90021-G"},{"key":"e_1_2_1_28_1","unstructured":"N. Dean and M. Hinchey. 1996. Teaching and Learning Formal Methods. Academic Press.  N. Dean and M. Hinchey. 1996. Teaching and Learning Formal Methods. Academic Press."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2010.10.020"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"M. B. Dwyer G. S. Avrunin and J. C. Corbett. 1998. Property specification patterns for finite-state verification. In FMSP. ACM 7--15.  M. B. Dwyer G. S. Avrunin and J. C. Corbett. 1998. Property specification patterns for finite-state verification. In FMSP. ACM 7--15.","DOI":"10.1145\/298595.298598"},{"key":"e_1_2_1_31_1","unstructured":"Event-b. 2018. Retrieved from http:\/\/www.event-b.org\/.  Event-b. 2018. Retrieved from http:\/\/www.event-b.org\/."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869542.1869625"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121207"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-018-9596-7"},{"key":"e_1_2_1_35_1","unstructured":"Eclipse foundation. 2015. Papyrus. Retrieved from https:\/\/eclipse.org\/papyrus\/.  Eclipse foundation. 2015. Papyrus. Retrieved from https:\/\/eclipse.org\/papyrus\/."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.65"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.90448"},{"key":"e_1_2_1_38_1","volume-title":"Lecture Notes in Computer Science","volume":"5846","author":"Gibbons J.","year":"2009","unstructured":"J. Gibbons and J. Nuno Oliveira ( Eds .). 2009 . TFM . Lecture Notes in Computer Science , Vol. 5846 . Springer. J. Gibbons and J. Nuno Oliveira (Eds.). 2009. TFM. Lecture Notes in Computer Science, Vol. 5846. Springer."},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"J. P. Gibson and D. M\u00e9ry. 1998. Teaching formal methods: Lessons to learn. In IWFM (Workshops in Computing). BCS.  J. P. Gibson and D. M\u00e9ry. 1998. Teaching formal methods: Lessons to learn. In IWFM (Workshops in Computing). BCS.","DOI":"10.14236\/ewic\/FM1998.4"},{"key":"e_1_2_1_40_1","volume-title":"Article 117 (Oct.","author":"Gleirscher Mario","year":"2019","unstructured":"Mario Gleirscher , Simon Foster , and Jim Woodcock . 2019. New opportunities for integrated formal methods. ACM Comput. Surv. 52, 6 , Article 117 (Oct. 2019 ), 36 pages. Mario Gleirscher, Simon Foster, and Jim Woodcock. 2019. New opportunities for integrated formal methods. ACM Comput. Surv. 52, 6, Article 117 (Oct. 2019), 36 pages."},{"key":"e_1_2_1_41_1","unstructured":"Mario Gleirscher and Diego Marmsoler. 2018. Formal methods: Oversold? Underused? A survey. arxiv:1812.08815. Retrieved from https:\/\/arxiv.orb\/abs\/1812.08815.  Mario Gleirscher and Diego Marmsoler. 2018. Formal methods: Oversold? Underused? A survey. arxiv:1812.08815. Retrieved from https:\/\/arxiv.orb\/abs\/1812.08815."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"R. Gmehlich K. Grau F. Loesch A. Iliasov M. Jackson and M. Mazzara. 2013. Towards a formalism-based toolkit for automotive applications. In FormaliSE@ICSE. IEEE Computer Society 36--42.  R. Gmehlich K. Grau F. Loesch A. Iliasov M. Jackson and M. Mazzara. 2013. Towards a formalism-based toolkit for automotive applications. In FormaliSE@ICSE. IEEE Computer Society 36--42.","DOI":"10.1109\/FormaliSE.2013.6612275"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"F. H.\n      Golra F.\n      Dagnat J.\n      Souqui\u00e8res I.\n      Sayar and \n      S.\n      Gu\u00e9rin\n  . \n  2018\n  . Bridging the gap between informal requirements and formal specifications using model federation. In SEFM Lecture Notes in Computer Science Vol. \n  10886\n  . \n  Springer 54--69.  F. H. Golra F. Dagnat J. Souqui\u00e8res I. Sayar and S. Gu\u00e9rin. 2018. Bridging the gap between informal requirements and formal specifications using model federation. In SEFM Lecture Notes in Computer Science Vol. 10886. Springer 54--69.","DOI":"10.1007\/978-3-319-92970-5_4"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"M. T. Grinder. 2002. Animating automata: A cross-platform program for teaching finite automata. In SIGCSE. ACM 63--67.  M. T. Grinder. 2002. Animating automata: A cross-platform program for teaching finite automata. In SIGCSE. ACM 63--67.","DOI":"10.1145\/563517.563364"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"R.\n      H\u00e4hnle K.\n      Johannisson and \n      A.\n      Ranta\n  . \n  2002\n  . An authoring tool for informal and formal requirements specifications. In FASE Lecture Notes in Computer Science Vol. \n  2306\n  . \n  Springer 233--248.  R. H\u00e4hnle K. Johannisson and A. Ranta. 2002. An authoring tool for informal and formal requirements specifications. In FASE Lecture Notes in Computer Science Vol. 2306. Springer 233--248.","DOI":"10.1007\/3-540-45923-5_16"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.compedu.2010.09.008"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"R. M. Hierons K. Bogdanov J. P. Bowen R. Cleaveland J. Derrick J. Dick M. Gheorghe M. Harman K. Kapoor P. J. Krause G. L\u00fcttgen A. J. H. Simons S. A. Vilkomir M. R. Woodward and H. Zedan. 2009. Using formal specifications to support testing. ACM Comput. Surv. 41 2 (2009) 9:1--9:76.  R. M. Hierons K. Bogdanov J. P. Bowen R. Cleaveland J. Derrick J. Dick M. Gheorghe M. Harman K. Kapoor P. J. Krause G. L\u00fcttgen A. J. H. Simons S. A. Vilkomir M. R. Woodward and H. Zedan. 2009. Using formal specifications to support testing. ACM Comput. Surv. 41 2 (2009) 9:1--9:76.","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_50_1","volume-title":"Software Pioneers","author":"Hoare C. A. R.","unstructured":"C. A. R. Hoare . 2002. An axiomatic basis for computer programming (reprint) . In Software Pioneers . Springer , Berlin , 367--383. C. A. R. Hoare. 2002. An axiomatic basis for computer programming (reprint). In Software Pioneers. Springer, Berlin, 367--383."},{"key":"e_1_2_1_51_1","unstructured":"IBM. 2020. Rational Doors. Retrieved from https:\/\/www.ibm.com\/products\/requirements-management.  IBM. 2020. Rational Doors. Retrieved from https:\/\/www.ibm.com\/products\/requirements-management."},{"key":"e_1_2_1_52_1","unstructured":"IBM. 2020. Rational Rhapsody 8.1.5. Retrieved from https:\/\/www.ibm.com\/products\/systems-design-rhapsody.  IBM. 2020. Rational Rhapsody 8.1.5. Retrieved from https:\/\/www.ibm.com\/products\/systems-design-rhapsody."},{"key":"e_1_2_1_53_1","first-page":"830","article-title":"IEEE Recommended Practice for Software Requirements Specifications","author":"IEEE.","year":"1998","unstructured":"IEEE. 1998 . IEEE Recommended Practice for Software Requirements Specifications , IEEE Std 830 - 1998 . DOI:https:\/\/doi.org\/10.1109\/IEEESTD.1998.88286 IEEE. 1998. IEEE Recommended Practice for Software Requirements Specifications, IEEE Std 830-1998. DOI:https:\/\/doi.org\/10.1109\/IEEESTD.1998.88286","journal-title":"IEEE Std"},{"key":"e_1_2_1_54_1","volume-title":"Standard - Systems and Software Engineering -- Life Cycle Processes --Requirements Engineering","author":"Int IEEE.","year":"2011","unstructured":"IEEE. 2011. ISO\/IEC\/IEEE Int . Standard - Systems and Software Engineering -- Life Cycle Processes --Requirements Engineering , ISO\/IEC\/IEEE 29148: 2011 (E), 2011. IEEE. 2011. ISO\/IEC\/IEEE Int. Standard - Systems and Software Engineering -- Life Cycle Processes --Requirements Engineering, ISO\/IEC\/IEEE 29148:2011(E), 2011."},{"key":"e_1_2_1_55_1","unstructured":"M. H. L. Wong Cheng In. 1994. Informal Semi-formal and Formal Approaches to the Specification of Software Requirements. MSc. Dissertation. University of British Columbia.  M. H. L. Wong Cheng In. 1994. Informal Semi-formal and Formal Approaches to the Specification of Software Requirements. MSc. Dissertation. University of British Columbia."},{"key":"e_1_2_1_56_1","volume-title":"TFM. Lecture Notes in Computer Science","volume":"5846","author":"Ishikawa F.","unstructured":"F. Ishikawa , K. Taguchi , N. Yoshioka , and S. Honiden . 2009. What top-level software engineers tackle after learning formal methods: Experiences from the top SE project . In TFM. Lecture Notes in Computer Science , Vol. 5846 . Springer, 57--71. F. Ishikawa, K. Taguchi, N. Yoshioka, and S. Honiden. 2009. What top-level software engineers tackle after learning formal methods: Experiences from the top SE project. In TFM. Lecture Notes in Computer Science, Vol. 5846. Springer, 57--71."},{"key":"e_1_2_1_57_1","unstructured":"D. Jackson. 2006. Software Abstractions\u2014Logic Language and Analysis. MIT Press.  D. Jackson. 2006. Software Abstractions\u2014Logic Language and Analysis. MIT Press."},{"key":"e_1_2_1_58_1","volume-title":"Problem Frames: Analyzing and Structuring Software Development Problems","author":"Jackson M.","unstructured":"M. Jackson . 2001. Problem Frames: Analyzing and Structuring Software Development Problems . Addison-Wesley . M. Jackson. 2001. Problem Frames: Analyzing and Structuring Software Development Problems. Addison-Wesley."},{"key":"e_1_2_1_59_1","volume-title":"Embedded World Conf. 6.","author":"Jeannet B.","unstructured":"B. Jeannet and F. Gaucher . 2015. Debugging real-time systems requirements: Simulate the \u201cwhat\u201d before the \u201chow .\u201d In Embedded World Conf. 6. B. Jeannet and F. Gaucher. 2015. Debugging real-time systems requirements: Simulate the \u201cwhat\u201d before the \u201chow.\u201d In Embedded World Conf. 6."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-014-0232-4"},{"key":"e_1_2_1_61_1","volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","unstructured":"L. Lamport . 2002. Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley . L. Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_2_1_62_1","volume-title":"Requirements Engineering for Software and Systems","author":"Laplante P.","unstructured":"P. Laplante . 2017. Requirements Engineering for Software and Systems . Auerbach Publications . P. Laplante. 2017. Requirements Engineering for Software and Systems. Auerbach Publications."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0068-5"},{"key":"e_1_2_1_64_1","volume-title":"Formal Underpinnings of Java Workshop (at OOPSLA\u201998)","author":"Leavens Gary T.","year":"1998","unstructured":"Gary T. Leavens , Albert L. Baker , and Clyde Ruby . 1998 . JML: A Java modeling language . In Formal Underpinnings of Java Workshop (at OOPSLA\u201998) . 404--420. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. 1998. JML: A Java modeling language. In Formal Underpinnings of Java Workshop (at OOPSLA\u201998). 404--420."},{"key":"e_1_2_1_65_1","doi-asserted-by":"crossref","unstructured":"F. L.\n      Li J.\n      Horkoff A.\n      Borgida G.\n      Guizzardi L.\n      Liu and \n      J.\n      Mylopoulos\n  . \n  2015\n  . From stakeholder requirements to formal specifications through refinement. In REFSQ Lecture Notes in Computer Science Vol. \n  9013\n  . \n  Springer 164--180.  F. L. Li J. Horkoff A. Borgida G. Guizzardi L. Liu and J. Mylopoulos. 2015. From stakeholder requirements to formal specifications through refinement. In REFSQ Lecture Notes in Computer Science Vol. 9013. Springer 164--180.","DOI":"10.1007\/978-3-319-16101-3_11"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595453.1595457"},{"key":"e_1_2_1_67_1","doi-asserted-by":"crossref","unstructured":"M. Luckcuck M. Farrell L. A. Dennis C. Dixon and M. Fisher. 2019. Formal specification and verification of autonomous robotic systems: A survey. ACM Comput. Surv. 52 5 (2019) 100:1--100:41.  M. Luckcuck M. Farrell L. A. Dennis C. Dixon and M. Fisher. 2019. Formal specification and verification of autonomous robotic systems: A survey. ACM Comput. Surv. 52 5 (2019) 100:1--100:41.","DOI":"10.1145\/3342355"},{"key":"e_1_2_1_68_1","volume-title":"Analyzing software requirements errors in safety-critical, embedded systems","author":"Lutz R. R.","unstructured":"R. R. Lutz . 1993. Analyzing software requirements errors in safety-critical, embedded systems . In RE. IEEE Computer Society , 126--133. R. R. Lutz. 1993. Analyzing software requirements errors in safety-critical, embedded systems. In RE. IEEE Computer Society, 126--133."},{"key":"e_1_2_1_69_1","unstructured":"J. Magee and J. Kramer. 2006. Concurrency\u2014State Models and Java Programs (2. ed.). Wiley.  J. Magee and J. Kramer. 2006. Concurrency\u2014State Models and Java Programs (2. ed.). Wiley."},{"key":"e_1_2_1_70_1","first-page":"1","article-title":"An Event-B Formalization of KAOS Goal Refinement Patterns. [Research Report] TR-LACL-2010-1","volume":"12","author":"Matoussi A.","year":"2010","unstructured":"A. Matoussi , F. Gervais , and R. Laleau . 2010 . An Event-B Formalization of KAOS Goal Refinement Patterns. [Research Report] TR-LACL-2010-1 , LACL. Technical Report. University Paris 12. 1 -- 34 pages. A. Matoussi, F. Gervais, and R. Laleau. 2010. An Event-B Formalization of KAOS Goal Refinement Patterns. [Research Report] TR-LACL-2010-1, LACL. Technical Report. University Paris 12. 1--34 pages.","journal-title":"LACL. Technical Report. University Paris"},{"key":"e_1_2_1_71_1","doi-asserted-by":"crossref","unstructured":"A. Mavin P. Wilkinson A. Harwood and M. Novak. 2009. Easy approach to requirements syntax (EARS). In RE. IEEE Computer Society 317--322.  A. Mavin P. Wilkinson A. Harwood and M. Novak. 2009. Easy approach to requirements syntax (EARS). In RE. IEEE Computer Society 317--322.","DOI":"10.1109\/RE.2009.9"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.229776"},{"key":"e_1_2_1_73_1","volume-title":"Object-Oriented Software Construction (1st and","author":"Meyer B.","unstructured":"B. Meyer . 1988, 1997. Object-Oriented Software Construction (1st and 2 nd editions). Prentice Hall . B. Meyer. 1988, 1997. Object-Oriented Software Construction (1st and 2nd editions). Prentice Hall.","edition":"2"},{"key":"e_1_2_1_74_1","series-title":"Lecture Notes in Computer Science","volume-title":"Abstract State Machines","author":"Meyer B.","unstructured":"B. Meyer . 2003. A framework for proving contract-equipped classes . In Abstract State Machines , Lecture Notes in Computer Science , Vol. 2589 . Springer , 108--125. B. Meyer. 2003. A framework for proving contract-equipped classes. In Abstract State Machines, Lecture Notes in Computer Science, Vol. 2589. Springer, 108--125."},{"key":"e_1_2_1_75_1","volume-title":"Modeling and Quality in Req. Engineering (Glinz Festscrhift)","author":"Meyer B.","year":"2013","unstructured":"B. Meyer . 2013. Multirequirements. Modeling and Quality in Req. Engineering (Glinz Festscrhift) ( 2013 ). B. Meyer. 2013. Multirequirements. Modeling and Quality in Req. Engineering (Glinz Festscrhift) (2013)."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.296"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1351324996001337"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-004-0195-3"},{"key":"e_1_2_1_79_1","series-title":"Lecture Notes in Computer Science","volume-title":"A Calculus of Communicating Systems","author":"Milner R.","unstructured":"R. Milner . 1980. A Calculus of Communicating Systems . Lecture Notes in Computer Science , Vol. 92 . Springer . R. Milner. 1980. A Calculus of Communicating Systems. Lecture Notes in Computer Science, Vol. 92. Springer."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_1_81_1","unstructured":"Modelica. 2017. Retrieved from https:\/\/doc.modelica.org\/.  Modelica. 2017. Retrieved from https:\/\/doc.modelica.org\/."},{"key":"e_1_2_1_82_1","unstructured":"ModelioSoft. 2017. Retrieved from https:\/\/www.modeliosoft.com\/products\/modelio-sa-system-architects.html.  ModelioSoft. 2017. Retrieved from https:\/\/www.modeliosoft.com\/products\/modelio-sa-system-architects.html."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCB.2003.819485"},{"key":"e_1_2_1_84_1","volume-title":"JCKBSE, Frontiers in Artificial Intelligence and Applications","author":"Nakatani T.","unstructured":"T. Nakatani . 2008. Requirements engineering education for professional engineers . In JCKBSE, Frontiers in Artificial Intelligence and Applications , Vol. 180 . IOS Press , 495--504. T. Nakatani. 2008. Requirements engineering education for professional engineers. In JCKBSE, Frontiers in Artificial Intelligence and Applications, Vol. 180. IOS Press, 495--504."},{"key":"e_1_2_1_86_1","series-title":"Lecture Notes in Computer Science","volume-title":"TOOLS","author":"Naumchev A.","unstructured":"A. Naumchev . 2019. Object-oriented requirements: Reusable, understandable, verifiable . In TOOLS , Lecture Notes in Computer Science , Vol. 11771 . Springer , 150--162. A. Naumchev. 2019. Object-oriented requirements: Reusable, understandable, verifiable. In TOOLS, Lecture Notes in Computer Science, Vol. 11771. Springer, 150--162."},{"key":"e_1_2_1_87_1","doi-asserted-by":"crossref","unstructured":"A. Naumchev. 2019. Seamless object-oriented requirements. In SIBIRCON. 0743--0748.  A. Naumchev. 2019. Seamless object-oriented requirements. In SIBIRCON. 0743--0748.","DOI":"10.1109\/SIBIRCON48586.2019.8958211"},{"key":"e_1_2_1_88_1","doi-asserted-by":"crossref","unstructured":"A. Naumchev and B. Meyer. 2016. Complete contracts through specification drivers. In TASE. IEEE Computer Society 160--167.  A. Naumchev and B. Meyer. 2016. Complete contracts through specification drivers. In TASE. IEEE Computer Society 160--167.","DOI":"10.1109\/TASE.2016.13"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cola.2019.02.004"},{"key":"e_1_2_1_90_1","doi-asserted-by":"crossref","unstructured":"A.\n      Naumchev B.\n      Meyer and \n      V.\n      Rivera\n  . \n  2015\n  . Unifying requirements and code: An example. In Ershov Memorial Conference Lecture Notes in Computer Science Vol. \n  9609\n  . \n  Springer 233--244.  A. Naumchev B. Meyer and V. Rivera. 2015. Unifying requirements and code: An example. In Ershov Memorial Conference Lecture Notes in Computer Science Vol. 9609. Springer 233--244.","DOI":"10.1007\/978-3-319-41579-6_18"},{"key":"e_1_2_1_91_1","unstructured":"T. Nguyen. 2015. Verification of behavioural requirements for complex systems with FORM-L a MODELICA extension. In ICSSEA.  T. Nguyen. 2015. Verification of behavioural requirements for complex systems with FORM-L a MODELICA extension. In ICSSEA."},{"issue":"4","key":"e_1_2_1_92_1","first-page":"1","article-title":"Unified Modeling Language, Superstructure","volume":"2","author":"OMG.","year":"2011","unstructured":"OMG. 2011 . Unified Modeling Language, Superstructure , Version 2 . 4 . 1 . Retrieved from http:\/\/www.omg.org\/spec\/UML\/2.4.1. OMG. 2011. Unified Modeling Language, Superstructure, Version 2.4.1. Retrieved from http:\/\/www.omg.org\/spec\/UML\/2.4.1.","journal-title":"Version"},{"key":"e_1_2_1_93_1","unstructured":"OMG Sanford Friedenthal Alan Moore and Rick Steiner. 2008. SysMl Tutorial. Retrieved from http:\/\/www.omgsysml.org\/INCOSE-2008-OMGSysML-Tutorial-Final-revb.pdf.  OMG Sanford Friedenthal Alan Moore and Rick Steiner. 2008. SysMl Tutorial. Retrieved from http:\/\/www.omgsysml.org\/INCOSE-2008-OMGSysML-Tutorial-Final-revb.pdf."},{"key":"e_1_2_1_94_1","unstructured":"Object Management Group (OMG). 2007. OMG Systems Modeling Language (OMG SysML\u2122) V1.0. OMG Document Number: Formal\/2007-09-01. Retrieved from http:\/\/www.omg.org\/spec\/SysML\/1.0\/PDF.  Object Management Group (OMG). 2007. OMG Systems Modeling Language (OMG SysML\u2122) V1.0. OMG Document Number: Formal\/2007-09-01. Retrieved from http:\/\/www.omg.org\/spec\/SysML\/1.0\/PDF."},{"key":"e_1_2_1_95_1","unstructured":"Object Management Group (OMG). 2015. UML 2.5. Retrieved from http:\/\/www.omg.org\/spec\/UML\/2.5\/.  Object Management Group (OMG). 2015. UML 2.5. Retrieved from http:\/\/www.omg.org\/spec\/UML\/2.5\/."},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-013-0192-5"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2002.1.5.c6"},{"key":"e_1_2_1_98_1","volume-title":"The Future of Software Engineering","author":"Parnas D. Lorge","unstructured":"D. Lorge Parnas . 2010. Precise documentation: The key to better software . In The Future of Software Engineering . Springer , 125--148. D. Lorge Parnas. 2010. Precise documentation: The key to better software. In The Future of Software Engineering. Springer, 125--148."},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/356698.356702"},{"key":"e_1_2_1_100_1","first-page":"40","article-title":"Uppaal2k","volume":"70","author":"Pettersson P.","year":"2000","unstructured":"P. Pettersson and K\/ G. Larsen . 2000 . Uppaal2k . In Bull. Eur. Assoc. for Theoretical Computer Sc. , Vol. 70. 40 -- 44 . P. Pettersson and K\/ G. Larsen. 2000. Uppaal2k. In Bull. Eur. Assoc. for Theoretical Computer Sc., Vol. 70. 40--44.","journal-title":"Bull. Eur. Assoc. for Theoretical Computer Sc."},{"key":"e_1_2_1_101_1","volume-title":"Overture Tool: Formal Modelling in VDM.","author":"Project The Overture","year":"2017","unstructured":"The Overture Project . 2017 . Overture Tool: Formal Modelling in VDM. Retrieved from http:\/\/overturetool.org\/method\/. The Overture Project. 2017. Overture Tool: Formal Modelling in VDM. Retrieved from http:\/\/overturetool.org\/method\/."},{"key":"e_1_2_1_102_1","unstructured":"Prot\u00e9g\u00e9. 2016. Retrieved from https:\/\/protege.stanford.edu\/.  Prot\u00e9g\u00e9. 2016. Retrieved from https:\/\/protege.stanford.edu\/."},{"key":"e_1_2_1_103_1","volume-title":"Grammatical Framework\u2014Programming with Multilingual Grammars","author":"Ranta Aarne","unstructured":"Aarne Ranta . 2011. Grammatical Framework\u2014Programming with Multilingual Grammars . Cambridge University Press . Aarne Ranta. 2011. Grammatical Framework\u2014Programming with Multilingual Grammars. Cambridge University Press."},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.008"},{"key":"e_1_2_1_105_1","doi-asserted-by":"crossref","unstructured":"J. N.\n      Reed\n     and \n      J. E.\n      Sinclair\n  . \n  2004\n  . Motivating study of formal methods in the classroom. In TFM Lecture Notes in Computer Science Vol. \n  3294\n  . \n  Springer 32--46.  J. N. Reed and J. E. Sinclair. 2004. Motivating study of formal methods in the classroom. In TFM Lecture Notes in Computer Science Vol. 3294. Springer 32--46.","DOI":"10.1007\/978-3-540-30472-2_3"},{"key":"e_1_2_1_106_1","unstructured":"Respect-it. 2011. Objectiver V3. Retrieved from http:\/\/www.objectiver.com.  Respect-it. 2011. Objectiver V3. Retrieved from http:\/\/www.objectiver.com."},{"key":"e_1_2_1_107_1","doi-asserted-by":"crossref","unstructured":"A. B. Romanovsky and M. Thomas (Eds.). 2013. Industrial Deployment of System Engineering Methods. Springer.  A. B. Romanovsky and M. Thomas (Eds.). 2013. Industrial Deployment of System Engineering Methods. Springer.","DOI":"10.1007\/978-3-642-33170-1"},{"key":"e_1_2_1_108_1","volume-title":"The Theory and Practice of Concurrency","author":"Roscoe A. W.","unstructured":"A. W. Roscoe . 1997. The Theory and Practice of Concurrency . Prentice Hall . A. W. Roscoe. 1997. The Theory and Practice of Concurrency. Prentice Hall."},{"key":"e_1_2_1_109_1","volume-title":"INCOSE Springer Symp. 10","author":"Schneider R. E.","year":"2000","unstructured":"R. E. Schneider and D. M. Buede . 2000. Properties of a high quality informal requirements document . INCOSE Springer Symp. 10 , 1 ( Jul. 2000 ), 352--359. R. E. Schneider and D. M. Buede. 2000. Properties of a high quality informal requirements document. INCOSE Springer Symp. 10, 1 (Jul. 2000), 352--359."},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0265-0"},{"key":"e_1_2_1_111_1","unstructured":"W. Scott and S. Cook. 2004. A context-free requirements grammar to facilitate automatic assessment. In AWRE. 4.1--4.10.  W. Scott and S. Cook. 2004. A context-free requirements grammar to facilitate automatic assessment. In AWRE. 4.1--4.10."},{"key":"e_1_2_1_112_1","doi-asserted-by":"crossref","unstructured":"J. Slankas and L. Williams. 2013. Automated extraction of non-functional requirements in available documentation. In NaturaLiSE. IEEE Computer Society 9--16.  J. Slankas and L. Williams. 2013. Automated extraction of non-functional requirements in available documentation. In NaturaLiSE. IEEE Computer Society 9--16.","DOI":"10.1109\/NAturaLiSE.2013.6611715"},{"key":"e_1_2_1_113_1","unstructured":"SPIN \/ Promela. 2020. Retrieved from http:\/\/spinroot.com\/spin\/Man\/promela.html.  SPIN \/ Promela. 2020. Retrieved from http:\/\/spinroot.com\/spin\/Man\/promela.html."},{"key":"e_1_2_1_114_1","volume-title":"State Chart XML (SCXML): State Machine Notation for Control Abstraction. W3C Working Draft","author":"State Chart XML","year":"2012","unstructured":"State Chart XML (SCXML) 2012. State Chart XML (SCXML): State Machine Notation for Control Abstraction. W3C Working Draft 16 February 2012 . Retrieved from https:\/\/www.w3.org\/TR\/scxml\/. State Chart XML (SCXML) 2012. State Chart XML (SCXML): State Machine Notation for Control Abstraction. W3C Working Draft 16 February 2012. Retrieved from https:\/\/www.w3.org\/TR\/scxml\/."},{"key":"e_1_2_1_115_1","unstructured":"Stimulus. 2015. Retrieved from http:\/\/argosim.com\/product-overview\/.  Stimulus. 2015. Retrieved from http:\/\/argosim.com\/product-overview\/."},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1145\/964723.383071"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0400-3"},{"key":"e_1_2_1_118_1","unstructured":"Dassault Systems. 2016. CATIA Reqtify. Retrieved from https:\/\/www.3ds.com\/products-services\/catia\/products\/reqtify.  Dassault Systems. 2016. CATIA Reqtify. Retrieved from https:\/\/www.3ds.com\/products-services\/catia\/products\/reqtify."},{"key":"e_1_2_1_119_1","unstructured":"Sparx Systems. 2017. Enterprise Architect. Retrieved from https:\/\/sparxsystems.eu\/enterprisearchitect\/system-requirements\/.  Sparx Systems. 2017. Enterprise Architect. Retrieved from https:\/\/sparxsystems.eu\/enterprisearchitect\/system-requirements\/."},{"key":"e_1_2_1_120_1","series-title":"Lecture Notes in Computer Science,Vol. 5846","volume-title":"Alloy: Using a kitchen example to teach Alloy with Z. In TFM","author":"Tarkan S.","year":"2009","unstructured":"S. Tarkan and V. Sazawal . 2009 . Chief chefs of Z to Alloy: Using a kitchen example to teach Alloy with Z. In TFM , Lecture Notes in Computer Science,Vol. 5846 . Springer , 72--91. S. Tarkan and V. Sazawal. 2009. Chief chefs of Z to Alloy: Using a kitchen example to teach Alloy with Z. In TFM, Lecture Notes in Computer Science,Vol. 5846. Springer, 72--91."},{"key":"e_1_2_1_121_1","series-title":"Lecture Notes in Computer Science","volume-title":"Eklund","author":"Tilley Thomas","year":"2005","unstructured":"Thomas Tilley , Richard Cole , Peter Becker , and Peter W . Eklund . 2005 . A survey of formal concept analysis support for software engineering activities. In Formal Concept Analysis, Lecture Notes in Computer Science , Vol. 3626 . Springer , 250--271. Thomas Tilley, Richard Cole, Peter Becker, and Peter W. Eklund. 2005. A survey of formal concept analysis support for software engineering activities. In Formal Concept Analysis, Lecture Notes in Computer Science, Vol. 3626. Springer, 250--271."},{"key":"e_1_2_1_122_1","doi-asserted-by":"crossref","unstructured":"N.\n      Tillmann F.\n      Chen and \n      W.\n      Schulte\n  . \n  2006\n  . Discovering likely method specifications. In ICFEM Lecture Notes in Computer Science Vol. \n  4260\n  . \n  Springer 717--736.  N. Tillmann F. Chen and W. Schulte. 2006. Discovering likely method specifications. In ICFEM Lecture Notes in Computer Science Vol. 4260. Springer 717--736.","DOI":"10.1007\/11901433_39"},{"key":"e_1_2_1_123_1","volume-title":"TAP, Lecture Notes in Computer Science","author":"Tillmann N.","unstructured":"N. Tillmann and J. de Halleux . 2008. Pex-white box test generation for .NET . In TAP, Lecture Notes in Computer Science , Vol. 4966 . Springer , 134--153. N. Tillmann and J. de Halleux. 2008. Pex-white box test generation for .NET. In TAP, Lecture Notes in Computer Science, Vol. 4966. Springer, 134--153."},{"key":"e_1_2_1_124_1","doi-asserted-by":"crossref","unstructured":"N. Tillmann and W. Schulte. 2005. Parameterized unit tests. In ESEC\/SIGSOFT FSE. ACM 253--262.  N. Tillmann and W. Schulte. 2005. Parameterized unit tests. In ESEC\/SIGSOFT FSE. ACM 253--262.","DOI":"10.1145\/1095430.1081749"},{"key":"e_1_2_1_125_1","doi-asserted-by":"crossref","unstructured":"J.\n      Tschannen C. A.\n      Furia M.\n      Nordio and \n      N.\n      Polikarpova\n  . \n  2015\n  . AutoProof: \n  Auto-active\n   functional verification of object-oriented programs. In TACAS Lecture Notes in Computer Science Vol. 9035. \n  Springer 566--580.  J. Tschannen C. A. Furia M. Nordio and N. Polikarpova. 2015. AutoProof: Auto-active functional verification of object-oriented programs. In TACAS Lecture Notes in Computer Science Vol. 9035. Springer 566--580.","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"e_1_2_1_126_1","doi-asserted-by":"crossref","unstructured":"A. van Lamsweerde. 2000. Formal specification: A roadmap. In ICSE\u2013Future of SE Track. ACM 147--159.  A. van Lamsweerde. 2000. Formal specification: A roadmap. In ICSE\u2013Future of SE Track. ACM 147--159.","DOI":"10.1145\/336512.336546"},{"key":"e_1_2_1_127_1","volume-title":"Goal-oriented requirements engineering: A guided tour","author":"van Lamsweerde A.","unstructured":"A. van Lamsweerde . 2001. Goal-oriented requirements engineering: A guided tour . In RE. IEEE Computer Society , 249. A. van Lamsweerde. 2001. Goal-oriented requirements engineering: A guided tour. In RE. IEEE Computer Society, 249."},{"key":"e_1_2_1_128_1","volume-title":"Goal-oriented requirements engineering: A roundtrip from research to practice","author":"van Lamsweerde A.","unstructured":"A. van Lamsweerde . 2004. Goal-oriented requirements engineering: A roundtrip from research to practice . In RE.IEEE Computer Society , 4--8. A. van Lamsweerde. 2004. Goal-oriented requirements engineering: A roundtrip from research to practice. In RE.IEEE Computer Society, 4--8."},{"key":"e_1_2_1_129_1","series-title":"Lecture Notes in Computer Science,Vol. 863","volume-title":"FTRTFT","author":"von der Beeck M.","unstructured":"M. von der Beeck . 1994. A comparison of statecharts variants . In FTRTFT , Lecture Notes in Computer Science,Vol. 863 . Springer , 128--148. M. von der Beeck. 1994. A comparison of statecharts variants. In FTRTFT, Lecture Notes in Computer Science,Vol. 863. Springer, 128--148."},{"key":"e_1_2_1_130_1","volume-title":"RELAX: Incorporating uncertainty into the specification of self-adaptive systems","author":"Whittle J.","year":"2009","unstructured":"J. Whittle , P. Sawyer , N. Bencomo , B. H. C. Cheng , and J.M. Bruel . 2009 . RELAX: Incorporating uncertainty into the specification of self-adaptive systems . In RE. IEEE Computer Society , 79--88. J. Whittle, P. Sawyer, N. Bencomo, B. H. C. Cheng, and J.M. Bruel. 2009. RELAX: Incorporating uncertainty into the specification of self-adaptive systems. In RE. IEEE Computer Society, 79--88."},{"key":"e_1_2_1_131_1","unstructured":"K. Wiegers and J. Beatty. 2013. Software Requirements. Pearson Education.  K. Wiegers and J. Beatty. 2013. Software Requirements. Pearson Education."},{"key":"e_1_2_1_132_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.17803"},{"key":"e_1_2_1_133_1","volume-title":"Juan Bicarregui, and John S. Fitzgerald.","author":"Woodcock Jim","year":"2009","unstructured":"Jim Woodcock , Peter Gorm Larsen , Juan Bicarregui, and John S. Fitzgerald. 2009 . Formal methods: Practice and experience. ACM Comput. Surv . 41, 4 (2009), 19:1--19:36. Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. 2009. Formal methods: Practice and experience. ACM Comput. Surv. 41, 4 (2009), 19:1--19:36."},{"key":"e_1_2_1_134_1","volume-title":"Towards modelling and reasoning support for early-phase requirements engineering","author":"E. Yu.","unstructured":"E. Yu. 1997. Towards modelling and reasoning support for early-phase requirements engineering . In ISRE. IEEE Computer Society , 226--235. E. Yu. 1997. Towards modelling and reasoning support for early-phase requirements engineering. In ISRE. IEEE Computer Society, 226--235."},{"key":"e_1_2_1_135_1","unstructured":"E. S. K. Yu and J. Mylopoulos. 1998. Why goal-oriented requirements engineering. In REFSQ. Presses Universitaires de Namur 15--22.  E. S. K. Yu and J. Mylopoulos. 1998. Why goal-oriented requirements engineering. In REFSQ. Presses Universitaires de Namur 15--22."},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2655056"},{"key":"e_1_2_1_137_1","doi-asserted-by":"publisher","DOI":"10.1145\/237432.237434"},{"key":"e_1_2_1_138_1","unstructured":"L. Zhao W. Alhoshan A. Ferrari K. J. Letsholo M. A. Ajagbe E. V. Chioasca and R. T. Batista-Navarro. 2020. Natural language processing (NLP) for requirements engineering: A systematic mapping study. CoRR abs\/2004.01099 (2020).  L. Zhao W. Alhoshan A. Ferrari K. J. Letsholo M. A. Ajagbe E. V. Chioasca and R. T. Batista-Navarro. 2020. Natural language processing (NLP) for requirements engineering: A systematic mapping study. CoRR abs\/2004.01099 (2020)."},{"key":"e_1_2_1_139_1","unstructured":"D. Zowghi and S. Paryani. 2003. Teaching requirements engineering through role playing: Lessons learnt. In RE. IEEE Computer Society 233.  D. Zowghi and S. Paryani. 2003. Teaching requirements engineering through role playing: Lessons learnt. In RE. IEEE Computer Society 233."}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3448975","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3448975","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:55Z","timestamp":1750193275000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3448975"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,25]]},"references-count":138,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,6,30]]}},"alternative-id":["10.1145\/3448975"],"URL":"https:\/\/doi.org\/10.1145\/3448975","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,5,25]]},"assertion":[{"value":"2020-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}