{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T21:59:46Z","timestamp":1770328786390,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107619","type":"print"},{"value":"9783032107626","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-10762-6_24","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T16:08:11Z","timestamp":1763222891000},"page":"313-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Use of\u00a0Certified Industrial Tools for\u00a0Formal Analysis and\u00a0Monitoring of\u00a0Communications-Based Train Control Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9698-5569","authenticated-orcid":false,"given":"Dalay","family":"Almeida","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Abrial, J.R., Lee, M., Neilson, D., Scharbach, P., S\u00f8rensen, I.: The b-method. In: Prehn, S., Toetenel, H. (eds.) VDM \u201991 Formal Software Development Methods. VDM 1991. LNCS, vol. 552, pp. 398\u2013405. Springer, Berlin, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0020001","DOI":"10.1007\/BFb0020001"},{"key":"24_CR2","doi-asserted-by":"publisher","unstructured":"Almeida, D., Jamain, F., Lecomte, T.: Formal analysis and monitoring of legacy safety-critical interlocking systems with the use of certified industrial Tools. In: Haxthausen, A.E., Serwe, W. (eds.) Formal Methods for Industrial Critical Systems. FMICS 2024. LNCS, vol. 14952, pp. 182\u2013198. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-68150-9_11","DOI":"10.1007\/978-3-031-68150-9_11"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Balcer, M., Hasling, W., Ostrand, T.: Automatic generation of test scripts from formal test specifications. In: Proceedings of the ACM SIGSOFT\u201989 Third Symposium on Software Testing, Analysis, and Verification, pp. 210\u2013218 (1989)","DOI":"10.1145\/75308.75332"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.: An entry point for formal methods: specification and analysis of event logs. arXiv preprint arXiv:1003.1682 (2010)","DOI":"10.4204\/EPTCS.20.2"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Batty, M.: Digital twins. Environ. Plan. B Urban Anal. City Sci. 45(5), 817\u2013820 (2018)","DOI":"10.1177\/2399808318796416"},{"key":"24_CR6","doi-asserted-by":"publisher","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.M.: Meteor: a successful application of b in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999 \u2013 Formal Methods. FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22","DOI":"10.1007\/3-540-48119-2_22"},{"issue":"3","key":"24_CR7","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10703-015-0226-3","volume":"46","author":"S Berkovich","year":"2015","unstructured":"Berkovich, S., Bonakdarpour, B., Fischmeister, S.: Runtime verification with minimal intrusion through parallelism. Form. Methods Syst. Des. 46(3), 317\u2013348 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0226-3","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Butler, M., et al.: The first twenty-five years of industrial use of the b-method. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) Formal Methods for Industrial Critical Systems. FMICS 2020. LNCS, vol. 12327, pp. 189\u2013209. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_8","DOI":"10.1007\/978-3-030-58298-2_8"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Cao, Y., Niu, R., Xu, T., Tang, T., Mu, J.: Wireless test platform of communication based train control (cbtc) system in urban mass transit. In: 2007 IEEE International Conference on Vehicular Electronics and Safety, pp.\u00a01\u20134. IEEE (2007)","DOI":"10.1109\/ICVES.2007.4456378"},{"key":"24_CR10","doi-asserted-by":"publisher","unstructured":"Chen, F., d\u2019Amorim, M., Ro\u015fu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) Formal Methods and Software Engineering. ICFEM 2004. LNCS, vol. 3308, pp. 357\u2013372. Springer, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_31","DOI":"10.1007\/978-3-540-30482-1_31"},{"key":"24_CR11","unstructured":"EN 50128:2011 Railway applications \u2013 Communication, signalling and processing systems \u2013 Software for railway control and protection systems (2011)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Greco, J.A.: Predict, detect and react to signaling and train control failures with improved diagnostics achieved with a suite of data collection and analysis tools in a maintenance and diagnostic center. In: ASME\/IEEE Joint Rail Conference, vol. 50978, p. V001T04A006. American Society of Mechanical Engineers (2018)","DOI":"10.1115\/JRC2018-6271"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Lecomte, T.: Atelier b. Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 35\u201346 (2014)","DOI":"10.1002\/9781119002727.ch2"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-030-48077-6_9","volume-title":"Rigorous State-Based Methods","author":"T Lecomte","year":"2020","unstructured":"Lecomte, T.: Programming the CLEARSY safety platform with B. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 124\u2013138. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_9"},{"key":"24_CR15","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102524","volume":"199","author":"T Lecomte","year":"2020","unstructured":"Lecomte, T., Deharbe, D., Fournier, P., Oliveira, M.: The clearsy safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199, 102524 (2020)","journal-title":"Sci. Comput. Program."},{"key":"24_CR16","unstructured":"Lecomte, T., et al.: Low cost high integrity platform. arXiv preprint arXiv:2005.07191 (2020)"},{"key":"24_CR17","unstructured":"Lin, Q., Xu, N.: Formal verification of train control procedures in train-centric cbtc system using colored petri nets. In: 2020 IEEE International Conference on Intelligent Rail Transportation (ICIRT), pp.\u00a01\u20136. IEEE (2020)"},{"issue":"1","key":"24_CR18","doi-asserted-by":"publisher","first-page":"154","DOI":"10.3141\/2289-20","volume":"2289","author":"X Liu","year":"2012","unstructured":"Liu, X., Saat, M.R., Barkan, C.P.: Analysis of causes of major train derailment and their effect on accident rates. Transp. Res. Rec. 2289(1), 154\u2013163 (2012)","journal-title":"Transp. Res. Rec."},{"issue":"1","key":"24_CR19","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10703-022-00401-y","volume":"59","author":"S Pinisetty","year":"2021","unstructured":"Pinisetty, S., Pradhan, A., Roop, P., Tripakis, S.: Compositional runtime enforcement revisited. Form. Methods Syst. Des. 59(1), 205\u2013252 (2021)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR20","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10703-013-0199-z","volume":"44","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., F\u00fcgger, M., Brauer, J.: Runtime verification of embedded real-time systems. Form. Methods Syst. Des. 44, 203\u2013239 (2014)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR21","unstructured":"Rushby, J., De\u00a0Moura, L.M., Hamon, G.: Formal methods for test case generation (Jan\u00a04 2011), uS Patent 7,865,339"},{"issue":"2","key":"24_CR22","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1109\/TSE.2020.2998503","volume":"48","author":"C Wang","year":"2020","unstructured":"Wang, C., Pastore, F., Goknil, A., Briand, L.C.: Automatic generation of acceptance test cases from use case specifications: an nlp-based approach. IEEE Trans. Softw. Eng. 48(2), 585\u2013616 (2020)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"8","key":"24_CR23","doi-asserted-by":"publisher","first-page":"931","DOI":"10.1049\/iet-its.2018.5231","volume":"12","author":"H Wang","year":"2018","unstructured":"Wang, H., Zhao, N., Ning, B., Tang, T., Chai, M.: Safety monitor for train-centric CBTC system. IET Intell. Transp. Syst. 12(8), 931\u2013938 (2018)","journal-title":"IET Intell. Transp. Syst."}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10762-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T16:23:40Z","timestamp":1764865420000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10762-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107619","9783032107626"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10762-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RSSRail","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reliability, Safety, and Security of Railway Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pisa","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rssrail2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rssrail2025.isti.cnr.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}