{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:07:04Z","timestamp":1767773224356,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T00:00:00Z","timestamp":1718668800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Excellence Laboratory \u201cInternational Centre for Mathematics and Computer Science in Toulouse\u201d"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2024,6,30]]},"abstract":"<jats:p>\n            The relationship between states (status of a system) and modes (capabilities of a system) used to describe system requirements is often poorly defined. The unclear relationship could make systems of interest out of control because of the out of boundaries of the systems caused by the newly added modes. Formally modeling and verifying requirements can clarify the relationship, making the system safer. To this end, an innovative approach to analyzing requirements is proposed. The\n            <jats:sc>\n              <jats:sans-serif>MoSt<\/jats:sans-serif>\n            <\/jats:sc>\n            language (a Domain Specific Language implemented on the Xtext framework) is firstly designed for requirements modeling and a model validator is realized to check requirements statically. A code generator is then provided to realize the automatic model transformation from the\n            <jats:sc>\n              <jats:sans-serif>MoSt<\/jats:sans-serif>\n            <\/jats:sc>\n            model to a NuSMV model, laying the foundation for the dynamic checks of requirements through symbolic model checking. Next, a NuSMV runner is designed to connect the NuSMV with the validator to automate the whole dynamic checks. The grammar, the model validator, the code generator, and the NuSMV runner are finally integrated into a publicly available Eclipse-based tool. Two case studies have been employed to illustrate the feasibility of our approach. For each case study, we injected 14 errors. The results show that the static and dynamic checks can successfully detect all the errors.\n          <\/jats:p>","DOI":"10.1145\/3640822","type":"journal-article","created":{"date-parts":[[2024,2,5]],"date-time":"2024-02-05T12:24:50Z","timestamp":1707135890000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Modeling and Verification of Natural Language Requirements based on States and Modes"],"prefix":"10.1145","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9711-2118","authenticated-orcid":false,"given":"Yinling","family":"Liu","sequence":"first","affiliation":[{"name":"CRAN, CNRS, Universite de Lorraine, Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3653-0148","authenticated-orcid":false,"given":"Jean-Michel","family":"Bruel","sequence":"additional","affiliation":[{"name":"IRIT, CNRS, Universite de Toulouse, Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,18]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2015.05.028"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2012.06.013"},{"key":"e_1_3_4_4_2","volume-title":"A Paradigm for General System Modeling and its Applications for UML and RM-ODP","author":"Andrey Naumenko","year":"2002","unstructured":"Naumenko Andrey. 2002. A Paradigm for General System Modeling and its Applications for UML and RM-ODP. Ph. D. Dissertation. Ph. D thesis."},{"key":"e_1_3_4_5_2","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/RE.2014.6912279","volume-title":"2014 IEEE 22nd International Requirements Engineering Conference (RE \u201914)","author":"Badger Julia","year":"2014","unstructured":"Julia Badger, David Throop, and Charles Claunch. 2014. VARED: Verification and analysis of requirements and early designs. In 2014 IEEE 22nd International Requirements Engineering Conference (RE \u201914). IEEE, 325\u2013326."},{"key":"e_1_3_4_6_2","volume-title":"An Integrated Model-based Early Validation Approach for Railway Systems","author":"Baduel Ronan","year":"2019","unstructured":"Ronan Baduel. 2019. An Integrated Model-based Early Validation Approach for Railway Systems. Ph. D. Dissertation. Toulouse 2."},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/3074444"},{"key":"e_1_3_4_8_2","first-page":"548","volume-title":"INCOSE International Symposium","author":"Bonnet St\u00e9phane","year":"2017","unstructured":"St\u00e9phane Bonnet, Jean-Luc Voirin, Daniel Exertier, and V\u00e9ronique Normand. 2017. Modeling system modes, states, configurations with Arcadia and Capella: Method and tool perspectives. In INCOSE International Symposium, Vol. 27. Wiley Online Library, 548\u2013562."},{"key":"e_1_3_4_9_2","volume-title":"The Engineering Design of Systems: Models and Methods","author":"Buede Dennis M.","year":"2016","unstructured":"Dennis M. Buede and William D. Miller. 2016. The Engineering Design of Systems: Models and Methods. John Wiley & Sons."},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0387-x"},{"key":"e_1_3_4_11_2","unstructured":"Roberto Cavada Alessandro Cimatti Gavin Keighren Emanuele Olivetti Marco Pistor and Marco Roveri. 2019. NuSMV 2.5 Tutorial. http:\/\/nusmv.fbk.eu\/NuSMV\/tutorial\/v25\/tutorial.pdf"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734431"},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734431"},{"key":"e_1_3_4_14_2","article-title":"IEEE standard glossary of software engineering terminology (IEEE Std 610.12-1990). Los Alamitos","volume":"169","author":"Committee IEEE Standards Coordinating","year":"1990","unstructured":"IEEE Standards Coordinating Committee. 1990. IEEE standard glossary of software engineering terminology (IEEE Std 610.12-1990). Los Alamitos. CA: IEEE Computer Society 169 (1990).","journal-title":"CA: IEEE Computer Society"},{"key":"e_1_3_4_15_2","first-page":"13","article-title":"SMC systems engineering primer & handbook","author":"Davis D.","year":"2005","unstructured":"D. Davis et\u00a0al. 2005. SMC systems engineering primer & handbook. United States Air Force Space & Missile Systems Center (2005), 13\u201317.","journal-title":"United States Air Force Space & Missile Systems Center"},{"key":"e_1_3_4_16_2","unstructured":"DFS. 2007. Unmanned Systems Safety Guide For DOD Acquisition. https:\/\/www.dau.edu\/cop\/esoh\/DAU%20Sponsored%20\\\\Documents\/Unmanned%20Systems%20Safety%20Guide%20forDOD%20Acquisition%2027June%202007.pdf"},{"key":"e_1_3_4_17_2","unstructured":"DI-IPSC-81431A. 2000. MIL-STD-498B (Cancelled) Data Item Description System\/Subsystem Specification."},{"key":"e_1_3_4_18_2","unstructured":"DMO. 2011. Defence Materiel Organisation DMH (ENG) 12-3-005 Function and Performance (FPS) Development Guide."},{"key":"e_1_3_4_19_2","volume-title":"Systems Engineering Test and Evaluation. Practical Approaches for Complex Systems Conference, Rydges Capital Hill, Canberra, Australia","author":"Edwards M. T.","year":"2003","unstructured":"M. T. Edwards. 2003. A practical approach to state and mode definitions for the specification and design of complex systems. In Systems Engineering Test and Evaluation. Practical Approaches for Complex Systems Conference, Rydges Capital Hill, Canberra, Australia."},{"key":"e_1_3_4_20_2","first-page":"1","article-title":"DAREF: MDA framework for modelling data warehouse requirements and deducing the multidimensional schema","author":"Beggar Omar El","year":"2020","unstructured":"Omar El Beggar, Khadija Letrache, and Mohammed Ramdani. 2020. DAREF: MDA framework for modelling data warehouse requirements and deducing the multidimensional schema. Requirements Engineering (2020), 1\u201323.","journal-title":"Requirements Engineering"},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD-CCA-ISIC.2006.4776814"},{"key":"e_1_3_4_22_2","doi-asserted-by":"crossref","first-page":"106590","DOI":"10.1016\/j.infsof.2021.106590","article-title":"Automated formalization of structured natural language requirements","author":"Giannakopoulou Dimitra","year":"2021","unstructured":"Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, and Johann Schumann. 2021. Automated formalization of structured natural language requirements. Information and Software Technology (2021), 106590.","journal-title":"Information and Software Technology"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2008.22"},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_3_4_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/234426.234431"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"e_1_3_4_27_2","article-title":"ISO\/IEC\/IEEE 24765: 2010 systems and software engineering-Vocabulary. ISO\/IEC\/IEEE 24765: 2010 25021","author":"24765 IEEE Standards Association IEEE","year":"2010","unstructured":"IEEE Standards Association IEEE 24765. 2010. ISO\/IEC\/IEEE 24765: 2010 systems and software engineering-Vocabulary. ISO\/IEC\/IEEE 24765: 2010 25021. Institute of Electrical and Electronics Engineers, Inc. (2010).","journal-title":"Institute of Electrical and Electronics Engineers, Inc."},{"key":"e_1_3_4_28_2","unstructured":"J. Jenney. 2011. Define Life Cycle System Modes. http:\/\/themanagersguide.blogspot.com\/2011\/01\/6322-define-life-cycle-system-modes.htmlaccessed on 25\/11\/2020."},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029905"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.317428"},{"key":"e_1_3_4_31_2","first-page":"190","volume-title":"2022 IEEE 30th International Requirements Engineering Conference Workshops (REW \u201922)","author":"Liu Yinling","year":"2022","unstructured":"Yinling Liu and Jean-Michel Bruel. 2022. Modeling of natural language requirements based on states and modes. In 2022 IEEE 30th International Requirements Engineering Conference Workshops (REW \u201922). IEEE, 190\u2013194."},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2009.9"},{"key":"e_1_3_4_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-019-00316-x"},{"key":"e_1_3_4_34_2","first-page":"1","article-title":"Modeling machine learning requirements from three perspectives: A case report from the healthcare domain","author":"Nalchigar Soroosh","year":"2021","unstructured":"Soroosh Nalchigar, Eric Yu, and Karim Keshavjee. 2021. Modeling machine learning requirements from three perspectives: A case report from the healthcare domain. Requirements Engineering (2021), 1\u201318.","journal-title":"Requirements Engineering"},{"key":"e_1_3_4_35_2","volume-title":"Systems Engineering\/Test and Evaluation Conference, Adela\u00efde, Australia","author":"Olver Anthony M.","year":"2014","unstructured":"Anthony M. Olver and Michael J. Ryan. 2014. On a useful taxonomy of phases, modes, and states in systems engineering. In Systems Engineering\/Test and Evaluation Conference, Adela\u00efde, Australia."},{"key":"e_1_3_4_36_2","volume-title":"Grammatical Framework: Programming with Multilingual Grammars","author":"Ranta Aarne","year":"2011","unstructured":"Aarne Ranta. 2011. Grammatical Framework: Programming with Multilingual Grammars. Vol. 173. CSLI Publications, Center for the Study of Language and Information Stanford."},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/41765.41801"},{"key":"e_1_3_4_38_2","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/1988008.1988018","volume-title":"Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-managing Systems","author":"Souza V\u00edtor E. Silva","year":"2011","unstructured":"V\u00edtor E. Silva Souza, Alexei Lapouchnian, William N. Robinson, and John Mylopoulos. 2011. Awareness requirements for adaptive systems. In Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-managing Systems. 60\u201369."},{"key":"e_1_3_4_39_2","article-title":"System phases, modes, and states solutions to controversial issues","author":"Wasson Charles S.","year":"2010","unstructured":"Charles S. Wasson. 2010. System phases, modes, and states solutions to controversial issues. Wasson Strategics, LLChttp:\/\/www.wassonstrategics.com (2010).","journal-title":"Wasson Strategics, LLC"},{"key":"e_1_3_4_40_2","volume-title":"System Engineering Analysis, Design, and Development: Concepts, Principles, and Practices","author":"Wasson Charles S.","year":"2015","unstructured":"Charles S. Wasson. 2015. System Engineering Analysis, Design, and Development: Concepts, Principles, and Practices. John Wiley & Sons."},{"key":"e_1_3_4_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2009.36"},{"key":"e_1_3_4_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISRE.1997.566873"},{"key":"e_1_3_4_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCSA.2010.62"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3640822","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3640822","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:41Z","timestamp":1750287041000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3640822"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,18]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6,30]]}},"alternative-id":["10.1145\/3640822"],"URL":"https:\/\/doi.org\/10.1145\/3640822","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2024,6,18]]},"assertion":[{"value":"2021-12-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-12","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}