{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:32Z","timestamp":1779074612327,"version":"3.51.4"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032120854","type":"print"},{"value":"9783032120861","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"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-12086-1_11","type":"book-chapter","created":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T08:36:10Z","timestamp":1764146170000},"page":"196-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Development of\u00a0a\u00a0Safety Controller for\u00a0Machine Learning Outputs in\u00a0Vital Railway Systems"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Lecomte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,27]]},"reference":[{"key":"11_CR1","unstructured":"Abrial, J.: The B-book - Assigning Programs to Meanings. Cambridge University Press (2005)"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., et al.: Formal methods in industry. Form. Asp. Comput. 37(1) (2024). https:\/\/doi.org\/10.1145\/3689374","DOI":"10.1145\/3689374"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, FM\u201999, Toulouse, France, 20\u201324 September 1999, Proceedings, Volume I. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22","DOI":"10.1007\/3-540-48119-2_22"},{"key":"11_CR4","unstructured":"Boulanger, J.: Safety of Computer Architectures. Wiley (2010)"},{"key":"11_CR5","doi-asserted-by":"crossref","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, pp. 189\u2013209. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-58298-2_8"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Comptier, M., Deharbe, D., Perez, J.M., Mussat, L., Pierre, T., Sabatier, D.: Safety analysis of a CBTC system: a rigorous approach with event-B. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, RSSRail 2017. LNCS, vol, 10598. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_10","DOI":"10.1007\/978-3-319-68499-4_10"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Comptier, M., Leuschel, M., Mejia, L.F., Perez, J., Mutz, M.: Property-Based Modelling and Validation of a CBTC Zone Controller in Event-B, pp. 202\u2013212, January (2019)","DOI":"10.1007\/978-3-030-18744-6_13"},{"key":"11_CR8","unstructured":"Dolle, D.: Les logiciels de s curit de trainguard mt cbtc. Le Rail 136, 34\u201339 (2007)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Forin, P.: Vital coded microprocessor principles and application for various transit systems. IFAC Proceedings Volumes 23(2), 79\u201384 (1990). iFAC\/IFIP\/IFORS Symposium on Control, Computers, Communications in Transportation, Paris, France, 19-21 September. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1474667017526531","DOI":"10.1016\/S1474-6670(17)52653-1"},{"key":"11_CR10","unstructured":"Jackson, D., et al.: Certified control: an architecture for verifiable safety of autonomous vehicles (2021). https:\/\/arxiv.org\/abs\/2104.06178"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-04570-7_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"T Lecomte","year":"2009","unstructured":"Lecomte, T.: Applying a formal method in industry: a 15-year trajectory. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 26\u201334. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04570-7_3"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"102524","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":"11_CR13","doi-asserted-by":"publisher","unstructured":"Lecomte, T., D\u00e9harbe, D., Prun, \u00c9., Mottin, E.: Applying a formal method in industry: a 25-year trajectory. In: da\u00a0Costa\u00a0Cavalheiro, S.A., Fiadeiro, J.L. (eds.) Formal Methods: Foundations and Applications - 20th Brazilian Symposium, Proceedings, SBMF 2017, Recife, Brazil, 29 November\u20131 December 2017. LNCS, vol. 10623, pp. 70\u201387. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-70848-5_6","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Ronneberger, O., Fischer, P., Brox, T.: U-Net: convolutional networks for biomedical image segmentation (2015). https:\/\/arxiv.org\/abs\/1505.04597","DOI":"10.1007\/978-3-319-24574-4_28"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Sabatier, D.: Using formal proof and b method at system level for industrial projects, pp. 20\u201331, June 2016","DOI":"10.1007\/978-3-319-33951-1_2"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-30885-7_34","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D Sabatier","year":"2012","unstructured":"Sabatier, D., Burdy, L., Requet, A., Gu\u00e9ry, J.: Formal proofs for the NYCT line 7 (flushing) modernization project. In: Derrick, J., et al. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 369\u2013372. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30885-7_34"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-12086-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T08:36:19Z","timestamp":1764146179000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-12086-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,27]]},"ISBN":["9783032120854","9783032120861"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-12086-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,27]]},"assertion":[{"value":"27 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Recife","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","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":"3 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sbmf2025.ufrpe.br\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}