{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T09:36:28Z","timestamp":1761989788273,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711763"},{"type":"electronic","value":"9783031711770"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>SCADE is both a formal language and a model-based development environment, widely used to build and verify the models of safety-critical system (SCS). The SCADE Design Verifier (DV) provides SAT-based verification. However, DV cannot adequately express complex temporal specifications, and it may fail due to complexity problems such as floating numbers which are often used in the aeronautics domain. In addition, manually writing temporal specifications is not only time-consuming but also error-prone. To address these challenges, we propose an AGVTS method that can automate the task of generating temporal specifications and verifying aeronautics SCADE models. At first, we define a modular pattern language for precisely expressing Chinese natural language requirements. Then, we present a rule-based translation augmented with BERT, which translates restricted requirements into LTL and CTL. In addition, SCADE model verification is achieved by transforming it into nuXmv which supports both SMT-based and SAT-based verification. Finally, we illustrate a successful application of our methodology with an ejection seat control system, and convince our industrial partners of the usefulness of formal methods for industrial systems.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_21","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"338-355","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["AGVTS: Automated Generation and\u00a0Verification of\u00a0Temporal Specifications for\u00a0Aeronautics SCADE Models"],"prefix":"10.1007","author":[{"given":"Hanfeng","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9888-6975","authenticated-orcid":false,"given":"Zhibin","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xilong","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weilin","family":"Deng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"issue":"7","key":"21_CR2","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1109\/TSE.2015.2398877","volume":"41","author":"M Autili","year":"2015","unstructured":"Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., Tang, A.: Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar. IEEE Trans. Softw. Eng. 41(7), 620\u2013638 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Basold, H., G\u00fcnther, H., Huhn, M., Milius, S.: An open alternative for SMT-based verification of scade models. In: Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings 19, pp. 124\u2013139. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10702-8_9","DOI":"10.1007\/978-3-319-10702-8_9"},{"key":"21_CR4","unstructured":"Bozzano, M., et al.: nuxmv 2.0. 0 user manual. fondazione bruno kessler. Tech. rep., Technical report, Trento, Italy (2019)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Chen, Y., Gandhi, R., Zhang, Y., Fan, C.: NL2TL: Transforming natural languages to temporal logics using large language models. In: Bouamor, H., Pino, J., Bali, K. (eds.) Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 15880\u201315903. Association for Computational Linguistics, Singapore (2023)","DOI":"10.18653\/v1\/2023.emnlp-main.985"},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Computer Aided Verification: 11th International Conference, CAV\u201999 Trento, Italy, July 6\u201310, 1999 Proceedings 11, pp. 495\u2013499. Springer (1999). https:\/\/doi.org\/10.1007\/s100090050046","DOI":"10.1007\/s100090050046"},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"21_CR8","unstructured":"Clarke, E.M., Heinle, W.: Modular Translation of Statecharts to SMV. Tech. rep, Citeseer (2000)"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.L., Pagano, B., Pouzet, M.: Scade 6: A formal language for embedded critical software development. In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 1\u201311. IEEE (2017)","DOI":"10.1109\/TASE.2017.8285623"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Conrad, E., Titolo, L., Giannakopoulou, D., Pressburger, T., Dutle, A.: A compositional proof framework for fretish requirements. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 68\u201381 (2022)","DOI":"10.1145\/3497775.3503685"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: interactively translating unstructured natural language to temporal logics with large language models. In: International Conference on Computer Aided Verification, pp. 383\u2013396. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Daskaya, I., Huhn, M., Milius, S.: Formal safety analysis in industrial practice. In: Formal Methods for Industrial Critical Systems: 16th International Workshop, FMICS 2011, Trento, Italy, August 29-30, 2011. Proceedings 16, pp. 68\u201384. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24431-5_7","DOI":"10.1007\/978-3-642-24431-5_7"},{"key":"21_CR13","unstructured":"Devlin, J., Chang, M.W., Lee, K., Toutanova, K.: Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint arXiv:1810.04805 (2018)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on Software engineering, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Fifarek, A.W., Wagner, L.G., Hoffman, J.A., Rodes, B.D., Aiello, M.A., Davis, J.A.: Spear v2. 0: formalized past LTL specification and analysis of requirements. In: NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings 9, pp. 420\u2013426. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_30","DOI":"10.1007\/978-3-319-57288-8_30"},{"key":"21_CR16","doi-asserted-by":"publisher","first-page":"106590","DOI":"10.1016\/j.infsof.2021.106590","volume":"137","author":"D Giannakopoulou","year":"2021","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Automated formalization of structured natural language requirements. Inf. Softw. Technol. 137, 106590 (2021). https:\/\/doi.org\/10.1016\/j.infsof.2021.106590","journal-title":"Inf. Softw. Technol."},{"issue":"6","key":"21_CR17","doi-asserted-by":"publisher","first-page":"1737","DOI":"10.1007\/s10270-023-01124-2","volume":"22","author":"M Gleirscher","year":"2023","unstructured":"Gleirscher, M., van de Pol, J., Woodcock, J.: A manifesto for applicable formal methods. Softw. Syst. Model. 22(6), 1737\u20131749 (2023)","journal-title":"Softw. Syst. Model."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"He, J., Bartocci, E., Ni\u010dkovi\u0107, D., Isakovic, H., Grosu, R.: Deepstl: from English requirements to signal temporal logic. In: Proceedings of the 44th International Conference on Software Engineering, pp. 610\u2013622 (2022)","DOI":"10.1145\/3510003.3510171"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering, pp. 372\u2013381 (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"21_CR20","unstructured":"Leveson, N.G.: Engineering a safer world: systems thinking applied to safety, The MIT Press (2016)"},{"key":"21_CR21","unstructured":"Mavridou, A., Bourbouh, H., Garoche, P.L., Giannakopoulou, D., Pessburger, T., Schumann, J.: Bridging the gap between requirements and Simulink model analysis. In: Joint 26th International Conference on Requirements Engineering: Foundation for Software Quality Workshops, Doctoral Symposium, Live Studies Track, and Poster Track (2020)"},{"key":"21_CR22","doi-asserted-by":"publisher","unstructured":"Nayak, A., Timmapathini, H.P., Murali, V., Ponnalagu, K., Venkoparao, V.G., Post, A.: Req2spec: transforming software requirements into formal specifications using natural language processing. In: International Working Conference on Requirements Engineering: Foundation for Software Quality, pp. 87\u201395. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-98464-9_8","DOI":"10.1007\/978-3-030-98464-9_8"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"21_CR24","unstructured":"Shi, J., Shi, J., Huang, Y., Xiong, J., She, Q.: Scade2nu: A tool for verifying safety requirements of scade models with temporal specifications. In: REFSQ Workshops (2019)"},{"key":"21_CR25","unstructured":"Wang, C., Ross, C., Kuo, Y.L., Katz, B., Barbu, A.: Learning a natural-language to LTL executable semantic parser for grounded robotics. In: Conference on Robot Learning, pp. 1706\u20131718. PMLR (2021)"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Yan, R., Cheng, C.H., Chai, Y.: Formal consistency checking over specifications in natural languages. In: 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1677\u20131682. IEEE (2015)","DOI":"10.7873\/DATE.2015.0452"},{"issue":"4","key":"21_CR27","doi-asserted-by":"publisher","first-page":"715","DOI":"10.1007\/s11704-017-6485-y","volume":"13","author":"Z Yang","year":"2019","unstructured":"Yang, Z., Bodeveix, J., Filali, M.: Towards a simple and safe objective caml compiling framework for the synchronous language SIGNAL. Frontiers Comput. Sci. 13(4), 715\u2013734 (2019)","journal-title":"Frontiers Comput. Sci."},{"issue":"1","key":"21_CR28","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s11704-015-4364-y","volume":"10","author":"Z Yang","year":"2016","unstructured":"Yang, Z., Bodeveix, J., Filali, M., Hu, K., Zhao, Y., Ma, D.: Towards a verified compiler prototype for the synchronous language SIGNAL. Frontiers Comput. Sci. 10(1), 37\u201353 (2016)","journal-title":"Frontiers Comput. Sci."},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, S., Zhai, J., Bu, L., Chen, M., Wang, L., Li, X.: Automated generation of LTL specifications for smart home IoT using natural language. In: 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 622\u2013625. IEEE (2020)","DOI":"10.23919\/DATE48585.2020.9116374"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:13:56Z","timestamp":1726121636000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}