{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T23:03:33Z","timestamp":1774479813237,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T00:00:00Z","timestamp":1604793600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,8]]},"DOI":"10.1145\/3368089.3417047","type":"proceedings-article","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T06:03:47Z","timestamp":1604815427000},"page":"1376-1386","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["FREPA: an automated and formal approach to requirement modeling and analysis in aircraft control domain"],"prefix":"10.1145","author":[{"given":"Jincao","family":"Feng","sequence":"first","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Weikai","family":"Miao","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Hanyue","family":"Zheng","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Yihao","family":"Huang","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Zheng","family":"Wang","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering, China"}]},{"given":"Ting","family":"Su","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Bin","family":"Gu","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering, China"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"Shanghai Trusted Industrial Control Platform, China"}]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[{"name":"China Academy of Space Technology, China"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]}],"member":"320","published-online":{"date-parts":[[2020,11,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"The B-book: assigning programs to meanings","author":"Abrial Jean-Raymond"},{"key":"e_1_3_2_2_2_1","volume-title":"Modeling in Event-B: system and software engineering","author":"Abrial Jean-Raymond"},{"key":"e_1_3_2_2_3_1","volume-title":"Success and Challenges. In International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. Springer, 31-35","author":"Abrial Jean-Raymond","year":"2018"},{"key":"e_1_3_2_2_4_1","unstructured":"SAE AS5506. 2004. Architecture analysis and design language (aadl). Embedded Computing Systems Committee SAE ( 2004 ).  SAE AS5506. 2004. Architecture analysis and design language (aadl). Embedded Computing Systems Committee SAE ( 2004 )."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_14"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14977-6_2"},{"key":"e_1_3_2_2_7_1","volume-title":"Formal Methods: State of the Art and New Directions","author":"B\u00f6rger Egon"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.935856"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Edmund M Clarke and Jeannette M Wing. 1996. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR) 28 4 ( 1996 ) 626-643.  Edmund M Clarke and Jeannette M Wing. 1996. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR) 28 4 ( 1996 ) 626-643.","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_2_2_11_1","volume-title":"Model checking","author":"Clarke Edmund M"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Darren Cofer Andrew Gacek John Backes Michael W Whalen Lee Pike Adam Foltzer Michal Podhradsky Gerwin Klein Ihor Kuz June Andronick etal 2018. A formal approach to constructing secure air vehicle software. Computer 51 11 ( 2018 ) 14-23.  Darren Cofer Andrew Gacek John Backes Michael W Whalen Lee Pike Adam Foltzer Michal Podhradsky Gerwin Klein Ihor Kuz June Andronick et al. 2018. A formal approach to constructing secure air vehicle software. Computer 51 11 ( 2018 ) 14-23.","DOI":"10.1109\/MC.2018.2876051"},{"key":"e_1_3_2_2_13_1","volume-title":"Goal-Directed Requirements Acquisition. In Selected Papers of the Sixth International Workshop on Software Specification and Design (6IWSSD). Elsevier Science Publishers B. V., NLD, 3-50","author":"Dardenne Anne","year":"1993"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Martin Davis George Logemann and Donald Loveland. 1962. A Machine Program for Theorem Proving. Communications of the Acm 5 7 ( 1962 ) 394-397.  Martin Davis George Logemann and Donald Loveland. 1962. A Machine Program for Theorem Proving. Communications of the Acm 5 7 ( 1962 ) 394-397.","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"crossref","unstructured":"BB Nicolau de Franca and G Horta Travassos. 2012. Reporting guidelines for simulation-based studies in software engineering. ( 2012 ).  BB Nicolau de Franca and G Horta Travassos. 2012. Reporting guidelines for simulation-based studies in software engineering. ( 2012 ).","DOI":"10.1049\/ic.2012.0019"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1647420.1647435"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2318202.2318210"},{"key":"e_1_3_2_2_19_1","unstructured":"Doors Document 2019. The document of the Engineering Requirements Management DOORS. https:\/\/www.ibm.com\/support\/knowledgecenter\/SSYQBZ_9.7.0\/ com.ibm.doors.requirements.doc\/helpindex_doors.html  Doors Document 2019. The document of the Engineering Requirements Management DOORS. https:\/\/www.ibm.com\/support\/knowledgecenter\/SSYQBZ_9.7.0\/ com.ibm.doors.requirements.doc\/helpindex_doors.html"},{"key":"e_1_3_2_2_20_1","volume-title":"2006 IEEE Conference on Computer Aided Control System Design, 2006 IEEE International Conference on Control Applications, 2006 IEEE International Symposium on Intelligent Control. IEEE, 1206-1211","author":"Feiler Peter H","year":"2006"},{"key":"e_1_3_2_2_21_1","first-page":"231","volume-title":"Statecharts: A visual formalism for complex systems. Science of computer programming 8, 3 ( 1987 )","author":"Harel David","year":"1987"},{"key":"e_1_3_2_2_22_1","volume-title":"A practical tutorial on modified condition\/decision coverage","author":"Hayhurst Kelly J"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00128"},{"key":"e_1_3_2_2_24_1","unstructured":"Takuto Ishimatsu Nancy G Leveson John Thomas Masa Katahira Yuko Miyamoto and Haruka Nakao. 2010. Modeling and hazard analysis using STPA. ( 2010 ).  Takuto Ishimatsu Nancy G Leveson John Thomas Masa Katahira Yuko Miyamoto and Haruka Nakao. 2010. Modeling and hazard analysis using STPA. ( 2010 )."},{"key":"e_1_3_2_2_25_1","volume-title":"The way of Z: practical programming with formal methods","author":"Jacky Jonathan"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2016.34"},{"key":"e_1_3_2_2_27_1","volume-title":"Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems","author":"Kelly John C"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939399.1939412"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Nancy Leveson. 2004. A new accident model for engineering safer systems. Safety science 42 4 ( 2004 ) 237-270.  Nancy Leveson. 2004. A new accident model for engineering safer systems. Safety science 42 4 ( 2004 ) 237-270.","DOI":"10.1016\/S0925-7535(03)00047-X"},{"key":"e_1_3_2_2_30_1","volume-title":"Integrating animation-based inspection into formal design specification construction for reliable software systems","author":"Li Mo","year":"2015"},{"key":"e_1_3_2_2_31_1","volume-title":"Formal Engineering for Industrial Software Development: Using the SOFL Method","author":"Liu Shaoying"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"crossref","DOI":"10.1109\/32.663996","article-title":"SOFL: A formal engineering methodology for industrial applications","volume":"24","author":"Liu Shaoying","year":"1998","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_3_2_2_33_1","article-title":"A formal engineering framework for service-based software modeling","volume":"6","author":"Miao Weikai","year":"2012","journal-title":"IEEE Transactions on Services Computing"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_3"},{"key":"e_1_3_2_2_35_1","unstructured":"Steven P Miller Timothy M Carlson and Alan C Tribble. 2003. Flight guidance system requirements specification. NASA.  Steven P Miller Timothy M Carlson and Alan C Tribble. 2003. Flight guidance system requirements specification. NASA."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2000.873688"},{"key":"e_1_3_2_2_37_1","unstructured":"Chris Newcombe Tim Rath Fan Zhang Bogdan Munteanu Marc Brooker and Michael Deardeuf. 2014. Use of formal methods at Amazon Web Services. See http:\/\/research. microsoft. com\/en-us\/um\/people\/lamport\/tla\/formal-methodsamazon. pdf ( 2014 ).  Chris Newcombe Tim Rath Fan Zhang Bogdan Munteanu Marc Brooker and Michael Deardeuf. 2014. Use of formal methods at Amazon Web Services. See http:\/\/research. microsoft. com\/en-us\/um\/people\/lamport\/tla\/formal-methodsamazon. pdf ( 2014 )."},{"key":"e_1_3_2_2_38_1","volume-title":"Quong","author":"Parr Terence J.","year":"1995"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Daniel Patrick Pereira Celso Hirata and Simin Nadjm-Tehrani. 2019. A STAMPbased ontology approach to support safety and security analyses. Journal of Information Security and Applications 47 ( 2019 ) 302-319.  Daniel Patrick Pereira Celso Hirata and Simin Nadjm-Tehrani. 2019. A STAMPbased ontology approach to support safety and security analyses. Journal of Information Security and Applications 47 ( 2019 ) 302-319.","DOI":"10.1016\/j.jisa.2019.05.014"},{"key":"e_1_3_2_2_40_1","volume-title":"The economic impacts of inadequate infrastructure for software testing","author":"Planning Strategic","year":"2002"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_2_43_1","unstructured":"RTCASE 2019. RTC's guide. http:\/\/www.visionmc.com\/  RTCASE 2019. RTC's guide. http:\/\/www.visionmc.com\/"},{"key":"e_1_3_2_2_44_1","unstructured":"SCADE Suite 2019. ANSYS SCADE Suite. https:\/\/www.ansys.com\/products\/ embedded-software\/ansys-scade-suite  SCADE Suite 2019. ANSYS SCADE Suite. https:\/\/www.ansys.com\/products\/ embedded-software\/ansys-scade-suite"},{"key":"e_1_3_2_2_45_1","volume-title":"Requirements engineering: a good practice guide","author":"Sommerville Ian"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3196478.3196485"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3306607"},{"key":"e_1_3_2_2_48_1","volume-title":"MDM: A mode diagram modeling framework. arXiv preprint arXiv:1301.0046 ( 2013 ).","author":"Wang Zheng","year":"2013"},{"key":"e_1_3_2_2_49_1","volume-title":"2014 Eighth International Conference on Software Security and Reliability (SERE). 118-126","author":"Wu T."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"crossref","unstructured":"Mengfei Yang Zheng Wang Geguang Pu Shengchao Qin Bin Gu and JiFeng He. 2012. The stochastic semantics and verification for periodic control systems. Science China Information Sciences 55 12 ( 2012 ) 2675-2693.  Mengfei Yang Zheng Wang Geguang Pu Shengchao Qin Bin Gu and JiFeng He. 2012. The stochastic semantics and verification for periodic control systems. Science China Information Sciences 55 12 ( 2012 ) 2675-2693.","DOI":"10.1007\/s11432-012-4750-0"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISRE.1997.566873"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183519.3183554"},{"key":"e_1_3_2_2_53_1","volume-title":"Working conference on verified software: Theories, tools, and experiments. Springer, 539-544","author":"Zhang Jian","year":"2005"}],"event":{"name":"ESEC\/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Virtual Event USA","acronym":"ESEC\/FSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3417047","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3368089.3417047","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:58Z","timestamp":1750197718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3417047"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,8]]},"references-count":52,"alternative-id":["10.1145\/3368089.3417047","10.1145\/3368089"],"URL":"https:\/\/doi.org\/10.1145\/3368089.3417047","relation":{},"subject":[],"published":{"date-parts":[[2020,11,8]]},"assertion":[{"value":"2020-11-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}