{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T03:05:37Z","timestamp":1770347137623,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031737084","type":"print"},{"value":"9783031737091","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-73709-1_12","type":"book-chapter","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T10:12:01Z","timestamp":1728382321000},"page":"186-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Can AI Help with\u00a0the\u00a0Formalization of\u00a0Railway Cybersecurity Requirements?"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0139-0421","authenticated-orcid":false,"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3270","authenticated-orcid":false,"given":"Gabriele","family":"Lenzini","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0591-877X","authenticated-orcid":false,"given":"Marinella","family":"Petrocchi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,9]]},"reference":[{"key":"12_CR1","unstructured":"Bartholomeus, M., et al.: The use of formal methods in specification and demonstration of ERTMS Hybrid Level 3. IRSE News 260, 14\u201317 (2019). https:\/\/www.irse.org\/LinkClick.aspx?fileticket=pKNpGWY33CA%3d&portalid=0"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-27008-7_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"D Basile","year":"2019","unstructured":"Basile, D., ter Beek, M.H., Ferrari, A., Legay, A.: Modelling and analysing ERTMS L3 moving block railway signalling with Simulink and Uppaal SMC. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 1\u201321. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_1"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-030-03421-4_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"D Basile","year":"2018","unstructured":"Basile, D., ter Beek, M.H., Ciancia, V.: Statistical model checking of a moving block railway signalling scenario with Uppaal SMC. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 372\u2013391. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_24"},{"key":"12_CR4","unstructured":"Brown, T.B., et\u00a0al.: Language models are few-shot learners. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems 33: Proceedings of the Annual Conference on Neural Information Processing Systems (NeurIPS 2020), pp. 1877\u20131901 (2020). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/1457c0d6bfcb4967418bfb8ac142f64a-Abstract.html"},{"key":"12_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-031-37703-7_18","volume-title":"CAV 2023","author":"M Cosler","year":"2023","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: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13965, pp. 383\u2013396. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18"},{"key":"12_CR6","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-93354-2_8","volume-title":"Information Systems Security and Privacy","author":"G Costantino","year":"2018","unstructured":"Costantino, G., Martinelli, F., Matteucci, I., Petrocchi, M.: Efficient detection of conflicts in data sharing agreements. In: Mori, P., Furnell, S., Camp, O. (eds.) ICISSP 2017. CCIS, vol. 867, pp. 148\u2013172. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-93354-2_8"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Fantechi, A., Gnesi, S., Passaro, L.C., Semini, L.: Inconsistency detection in natural language requirements using ChatGPT: a preliminary evaluation. In: Schneider, K., Dalpiaz, F., Horkoff, J. (eds.) Proceedings of the 31st IEEE International Requirements Engineering Conference (RE 2023), pp. 335\u2013340. IEEE (2023). https:\/\/doi.org\/10.1109\/RE57278.2023.00045","DOI":"10.1109\/RE57278.2023.00045"},{"key":"12_CR8","unstructured":"Fantechi, A., Gnesi, S., Semini, L.: Rule-based NLP vs ChatGPT in ambiguity detection, a preliminary study. In: Ferrari, A., et\u00a0al. (eds.) Joint Proceedings of REFSQ-2023 Workshops, Doctoral Symposium, Posters & Tools Track and Journal Early Feedback: 6th Workshop on Natural Language Processing for Requirements Engineering (NLP4RE 2023). CEUR Workshop Proceedings, vol.\u00a03378. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3378\/NLP4RE-paper1.pdf"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Ferrari, A., ter Beek, M.H.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55(4), 69:1\u201369:37 (2023). https:\/\/doi.org\/10.1145\/3520480","DOI":"10.1145\/3520480"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Lipari, G., Gnesi, S., Spagnolo, G.O.: Pragmatic ambiguity detection in natural language requirements. In: Bencomo, N., Cleland-Huang, J., Guo, J., Harrison, R. (eds.) Proceedings of the 1st International Workshop on Artificial Intelligence for Requirements Engineering (AIRE 2014), pp.\u00a01\u20138. IEEE (2014). https:\/\/doi.org\/10.1109\/AIRE.2014.6894849","DOI":"10.1109\/AIRE.2014.6894849"},{"issue":"11","key":"12_CR11","doi-asserted-by":"publisher","first-page":"4675","DOI":"10.1109\/TSE.2021.3124677","volume":"48","author":"A Ferrari","year":"2022","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H.: Systematic evaluation and usability analysis of formal methods tools for railway signaling system design. IEEE Trans. Softw. Eng. 48(11), 4675\u20134691 (2022). https:\/\/doi.org\/10.1109\/TSE.2021.3124677","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Spoletini, P., Gnesi, S.: Ambiguity cues in requirements elicitation interviews. In: Proceedings of the 24th International Conference on Requirements Engineering (RE 2016), pp. 56\u201365. IEEE (2016). https:\/\/doi.org\/10.1109\/RE.2016.25","DOI":"10.1109\/RE.2016.25"},{"key":"12_CR13","unstructured":"Furness, N., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS level\u00a03: the game-changer. IRSE News 232, 2\u20139 (2017). https:\/\/www.irse.nl\/resources\/170314-ERTMS-L3-The-gamechanger-from-IRSE-News-Issue-232.pdf"},{"key":"12_CR14","unstructured":"Gewirtz, D.: How to write better ChatGPT prompts in 5\u00a0steps. ZDNET (online magazine) (2024). https:\/\/www.zdnet.com\/article\/how-to-write-better-chatgpt-prompts-in-5-steps\/"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-319-06749-0_11","volume-title":"Privacy Technologies and Policy","author":"S Gnesi","year":"2014","unstructured":"Gnesi, S., Matteucci, I., Moiso, C., Mori, P., Petrocchi, M., Vescovi, M.: My data, your data, our data: managing privacy preferences in multiple subjects personal data. In: Preneel, B., Ikonomou, D. (eds.) APF 2014. LNCS, vol. 8450, pp. 154\u2013171. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06749-0_11"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Gnesi, S., Petrocchi, M.: Towards an executable algebra for product lines. In: Proceedings of the 16th International Software Product Line Conference (SPLC 2012), vol.\u00a02, pp. 66\u201373. ACM (2012). https:\/\/doi.org\/10.1145\/2364412.2364424","DOI":"10.1145\/2364412.2364424"},{"key":"12_CR17","unstructured":"International Union of Railways (UIC): ERTMS\/ETCS Systems Requirements Specification (1999)"},{"key":"12_CR18","unstructured":"Karia, R., Dobhal, D., Bramblett, D., Verma, P., Srivastava, S.: Can LLMs Converse Formally? Automatically Assessing LLMs in Translating and Interpreting Formal Specifications (2024). https:\/\/arxiv.org\/abs\/2403.18327"},{"key":"12_CR19","unstructured":"Krishna, M., Gaur, B., Verma, A., Jalote, P.: Using LLMs in Software Requirements Specifications: An Empirical Evaluation (2024). https:\/\/arxiv.org\/abs\/2404.17842"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-030-30985-5_29","volume-title":"From Software Engineering to Formal Methods and Tools, and Back","author":"G Lenzini","year":"2019","unstructured":"Lenzini, G., Petrocchi, M.: Modelling of railway signalling system requirements by controlled natural languages: a case study. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 502\u2013518. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30985-5_29"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Marques, N., Silva, R.R., Bernardino, J.: Using ChatGPT in software requirements engineering: a comprehensive review. Future Internet 16(6) (2024). https:\/\/doi.org\/10.3390\/fi16060180","DOI":"10.3390\/fi16060180"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-32498-7_42","volume-title":"Multidisciplinary Research and Practice for Information Systems","author":"F Martinelli","year":"2012","unstructured":"Martinelli, F., Matteucci, I., Petrocchi, M., Wiegand, L.: A formal support for collaborative data sharing. In: Quirchmayr, G., Basl, J., You, I., Xu, L., Weippl, E. (eds.) CD-ARES 2012. LNCS, vol. 7465, pp. 547\u2013561. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32498-7_42"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Matteucci, I., Petrocchi, M., Sbodio, M.L.: CNL4DSA: a controlled natural language for data sharing agreements. In: Shin, S.Y., Ossowski, S., Schumacher, M., Palakal, M.J., Hung, C. (eds.) Proceedings of the 25th Symposium on Applied Computing (SAC 2010), pp. 616\u2013620. ACM (2010). https:\/\/doi.org\/10.1145\/1774088.1774218","DOI":"10.1145\/1774088.1774218"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Sahoo, P., Singh, A.K., Saha, S., Jain, V., Mondal, S., Chadha, A.: A Systematic Survey of Prompt Engineering in Large Language Models: Techniques and Applications (2024). https:\/\/doi.org\/10.48550\/arXiv.2402.07927","DOI":"10.48550\/arXiv.2402.07927"},{"key":"12_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-031-19762-8_20","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Practice","author":"M Seisenberger","year":"2022","unstructured":"Seisenberger, M., et al.: Safe and secure future AI-driven railway technologies: challenges for formal methods in railway. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13704, pp. 246\u2013268. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19762-8_20"},{"key":"12_CR26","doi-asserted-by":"publisher","first-page":"92312","DOI":"10.1109\/ACCESS.2023.3309005","volume":"11","author":"S Soderi","year":"2023","unstructured":"Soderi, S., Masti, D., H\u00e4m\u00e4l\u00e4inen, M., Iinatti, J.H.: Cybersecurity considerations for communication based train control. IEEE Access 11, 92312\u201392321 (2023). https:\/\/doi.org\/10.1109\/ACCESS.2023.3309005","journal-title":"IEEE Access"},{"issue":"7","key":"12_CR27","doi-asserted-by":"publisher","first-page":"6764","DOI":"10.1109\/TITS.2023.3254442","volume":"24","author":"S Soderi","year":"2023","unstructured":"Soderi, S., Masti, D., Lun, Y.Z.: Railway cyber-security in the era of interconnected systems: a survey. IEEE Trans. Intell. Transp. Syst. 24(7), 6764\u20136779 (2023). https:\/\/doi.org\/10.1109\/TITS.2023.3254442","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"issue":"1\u20132","key":"12_CR28","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/S0004-3702(99)00037-5","volume":"111","author":"J Straach","year":"1999","unstructured":"Straach, J., Truemper, K.: Learning to ask relevant questions. Artif. Intell. 111(1\u20132), 301\u2013327 (1999). https:\/\/doi.org\/10.1016\/S0004-3702(99)00037-5","journal-title":"Artif. Intell."},{"key":"12_CR29","unstructured":"Vaswani, A., et al.: Attention is all you need. In: Guyon, I., et al. (eds.) Advances in Neural Information Processing Systems 30: Proceedings of the Annual Conference on Neural Information Processing Systems (NeurIPS 2017), pp. 5998\u20136008 (2017). https:\/\/proceedings.neurips.cc\/paper\/2017\/hash\/3f5ee243547dee91fbd053c1c4a845aa-Abstract.html"},{"key":"12_CR30","unstructured":"Vogelsang, A., Fischbach, J.: Using Large Language Models for Natural Language Processing Tasks in Requirements Engineering: A Systematic Guideline (2024). https:\/\/arxiv.org\/abs\/2402.13823"},{"key":"12_CR31","unstructured":"Vv.Aa.: Effective Prompts for AI: The Essentials. MIT Sloan Teaching & Learning Technologies (online magazine) (2023). https:\/\/mitsloanedtech.mit.edu\/ai\/basics\/effective-prompts\/"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73709-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T09:05:32Z","timestamp":1729674332000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73709-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,9]]},"ISBN":["9783031737084","9783031737091"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73709-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,9]]},"assertion":[{"value":"9 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}