{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:15:53Z","timestamp":1770336953012,"version":"3.49.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319050317","type":"print"},{"value":"9783319050324","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-05032-4_13","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T09:36:26Z","timestamp":1394184986000},"page":"167-183","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":45,"title":["Twenty-Five Years of Formal Methods and Railways: What Next?"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book. Cambridge University Press, New York (1996)"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"774","DOI":"10.1016\/j.tre.2007.04.001","volume":"44","author":"M Abril","year":"2008","unstructured":"Abril, M., Barber, F., Ingolotti, L., Salido, M.A., Tormos, P., Lova, A.: An assessment of railway capacity. Transp. Res. Part E-Logist. Transp. Rev. 44, 774\u2013806 (2008)","journal-title":"Transp. Res. Part E-Logist. Transp. Rev."},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10817-010-9172-3","volume":"45","author":"D Angeletti","year":"2010","unstructured":"Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. J. Autom. Reason. 45, 397\u2013414 (2010)","journal-title":"J. Autom. Reason."},{"key":"13_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/11813040_13","volume-title":"FM 2006","author":"S Bacherini","year":"2006","unstructured":"Bacherini, S., Fantechi, A., Tempestini, M., Zingoni, \u00f2: A story about formal methods adoption by a railway signaling manufacturer. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, pp. 179\u2013189. Springer, Heidelberg (2006)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Banci, M., Fantechi, A.: Instantiating generic charts for railway interlocking systems. In: Tenth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2005), Lisbon, 5\u20136, September 2005","DOI":"10.1145\/1081180.1081197"},{"key":"13_CR6","series-title":"LNCS","first-page":"369","volume-title":"FM 1999","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999)"},{"issue":"2","key":"13_CR7","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"C Bernardeschi","year":"1998","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., Romano, D.: A formal verification environment for railway signaling system design. Formal Methods Syst. Des. 12(2), 139\u2013161 (1998)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR8","series-title":"LNCS","first-page":"193","volume-title":"TACAS 1999","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M., Cipriani, L.: Validation of railway interlocking systems by formal verification, a case study. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013 Workshops. LNCS, vol. 8368, pp. XX\u2013XY (2013)","DOI":"10.1007\/978-3-319-05032-4_18"},{"key":"13_CR10","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1016\/j.trb.2005.09.004","volume":"40","author":"R Burdett","year":"2006","unstructured":"Burdett, R., Kozan, E.: Techniques for absolute capacity determination in railways. Transp. Res. Part B: Methodol. 40, 616\u2013632 (2006)","journal-title":"Transp. Res. Part B: Methodol."},{"key":"13_CR11","unstructured":"Cavada, R., Cimatti, A., Mariotti, A., Mattarei, C., Micheli, A., Mover, S., Pensallorto, M., Roveri, M., Susi, A., Tonetta, S.: EuRailCheck: tool support for requirements validation. In: ASE 2009, Auckland, New Zealand, 16\u201320, November 2009"},{"key":"13_CR12","unstructured":"CBMC. http:\/\/www.cprover.org\/cbmc\/"},{"key":"13_CR13","series-title":"LNCS","first-page":"378","volume-title":"CAV 2012","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A., Tchaltsev, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378\u2013393. Springer, Heidelberg (2012)"},{"key":"13_CR14","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR15","first-page":"238","volume-title":"In: Proceedings of 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201977","author":"P Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201977, pp. 238\u2013252. ACM, New York (1977)"},{"key":"13_CR16","unstructured":"DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: subway speed control system. In: Proceedings 5th IFIP Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992), Perros-Guirec, North-Holland, pp. 199\u2013213 (1993)"},{"key":"13_CR17","unstructured":"Deutsch, A.: Static verification of dynamic properties. Polyspace, White Paper (2004)"},{"key":"13_CR18","unstructured":"http:\/\/www.ertms.net"},{"key":"13_CR19","unstructured":"Esposito, R., Lazzaro, A., Marmo, P., Sanseviero, A.: Formal verification of ERTMS Euroradio safety critical protocol. In: 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u201903). L\u2019Harmattan, Budapest, Hongrie (2003)"},{"key":"13_CR20","volume-title":"EN50128, Railway Applications - Software for Railway Control and Protection Systems","author":"European Committee for Electrotechnical Standardization","year":"1997","unstructured":"European Committee for Electrotechnical Standardization: EN50128, Railway Applications - Software for Railway Control and Protection Systems. CENELEC, Brussels (1997)"},{"key":"13_CR21","volume-title":"EN50128, Railway Applications - Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems","author":"European Committee for Electrotechnical Standardization","year":"2011","unstructured":"European Committee for Electrotechnical Standardization: EN50128, Railway Applications - Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems. CENELEC, Brussels (2011)"},{"key":"13_CR22","series-title":"LNCS","first-page":"276","volume-title":"ISoLA 2012, Part II","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A.: Distributing the challenge of model checking interlocking control tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 276\u2013289. Springer, Heidelberg (2012)"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Fantechi, A., Fokkink, W., Morzenti, A.: Some trends in formal methods applications to railway signaling. In: Gnesi, S., Margaria, T. (eds.) Formal Methods for Industrial Critical Systems: A Survey of Applications. IEEE Computer Society Press, Los Alamitos, pp. 63\u201384 (2013)","DOI":"10.1002\/9781118459898.ch4"},{"key":"13_CR24","unstructured":"Ferrari, A., Fantechi, A., Bacherini, S., Zingoni, N.: Modeling guidelines for code generation in the railway signaling context. In: Proceedings of 1st Nasa Formal Methods Symposium, pp. 166\u2013170 (2009)"},{"issue":"3","key":"13_CR25","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/MS.2013.44","volume":"30","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Fantechi, A., Gnesi, S., Magnani, G.: Model-based development and formal methods in the railway industry. IEEE Softw. 30(3), 28\u201334 (2013)","journal-title":"IEEE Softw."},{"issue":"7","key":"13_CR26","doi-asserted-by":"publisher","first-page":"828","DOI":"10.1016\/j.scico.2012.04.003","volume":"78","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Grasso, D., Magnani, G., Fantechi, A., Tempestini, M.: The Metro Rio case study. Sci. Comput. Program. 78(7), 828\u2013842 (2013)","journal-title":"Sci. Comput. Program."},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Proceedings of the 8th FORMS\/FORMAT Symposium, pp. 98\u2013107 (2010)","DOI":"10.1007\/978-3-642-14261-1_11"},{"issue":"2","key":"13_CR28","first-page":"42","volume":"2","author":"A Ferrari","year":"2011","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A., Tempestini, M.: Adoption of model-based testing and abstract interpretation by a railway signalling manufacturer. IJERTCS 2(2), 42\u201361 (2011)","journal-title":"IJERTCS"},{"key":"13_CR29","unstructured":"Groote, J.F., van Vlijmen, S., Koorn, J.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Logic Group Preprint Series 121. Utrecht University (1995)"},{"key":"13_CR30","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"13_CR31","unstructured":"Hase, K.R.: Open proof for railway safety software - a potential way-out of vendor lock-in advancing to standardization, transparency, and software security. In: Proceedings of the 8th FORMS\/FORMAT Symposium, pp. 4\u201337 (2010)"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Haxthausen, A.E., Peleska, J., Pinger, R.: Applied bounded model checking for interlocking system designs. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013 Workshops. LNCS, vol. 8368, pp. XX\u2013YY (2013)","DOI":"10.1007\/978-3-319-05032-4_16"},{"issue":"8","key":"13_CR33","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1109\/32.879808","volume":"26","author":"AE Haxthausen","year":"2000","unstructured":"Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687\u2013701 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Iliasov, A., Romanovsky, A.: SafeCap domain language for reasoning about safety and capacity. Newcastle University, Computing Science, Technical Report Series, CS-TR-1352 (2012)","DOI":"10.1109\/WDTS-RASD.2012.11"},{"key":"13_CR35","unstructured":"FP7 Project INESS - Deliverable D.1.5 Report on translation of requirements from text to UML (2009)"},{"key":"13_CR36","unstructured":"FP7 Project INESS - Deliverable D.4.1 Documented strategy for Verification and Validation, Report (2009)"},{"key":"13_CR37","unstructured":"Institute of Electrical and Electronics Engineers: IEEE Standard for Communications Based Train Control (CBTC) Performance and Functional Requirements. IEEE Std 1474.1-2004"},{"key":"13_CR38","series-title":"LNCS","first-page":"54","volume-title":"IFM 2012","author":"Y Isobe","year":"2012","unstructured":"Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways - an approach in timed CSP. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 54\u201368. Springer, Heidelberg (2012)"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"James, P., Lawrence, A., Moller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., Chadwick, S.: Verification of solid state interlocking programs. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013 Workshops. LNCS, vol. 8368, pp. XX\u2013YY (2013)","DOI":"10.1007\/978-3-319-05032-4_19"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., Williams, D.: Verification of Scheme Plans using CSP$$||$$B. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013 Workshops. LNCS, vol. 8368, pp. XX\u2013YY (2013)","DOI":"10.1007\/978-3-319-05032-4_15"},{"issue":"4","key":"13_CR41","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009)","journal-title":"ACM Comput. Surv."},{"key":"13_CR42","unstructured":"Kontaxi, E., Ricci, S.: Railway capacity analysis; methodological framework and harmonization perspectives. In: Proceedings of the 12th World Conference on Transportation Research, Lisboa, July 2010"},{"key":"13_CR43","unstructured":"Mentre, D.: Evaluation model of ETCS using GNATprove, openETCS Technical Report June 2013"},{"key":"13_CR44","doi-asserted-by":"crossref","unstructured":"Pascoe, R.D., Eichorn, T.N.: What is Communication-Based Train Control? IEEE Vehicular Technology Magazine (2009)","DOI":"10.1109\/MVT.2009.934665"},{"key":"13_CR45","unstructured":"Sauvage, S., Bouali, A.: Development approaches in software development. In: Proceedings of ERTS, Toulouse (2006)"},{"key":"13_CR46","unstructured":"Simulink. http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"13_CR47","unstructured":"UK Ministry of Defence: Def Stan 00\u201355: Requirements for Safety Related Software in Defence Equipment, August 1997"},{"key":"13_CR48","unstructured":"Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool support for checking railway interlocking designs. In: Proceedings of the 10th Australian workshop on Safety critical systems and software, pp. 101\u2013107 (2006)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05032-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T22:13:34Z","timestamp":1675808014000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05032-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319050317","9783319050324"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05032-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}