{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:13Z","timestamp":1773827473667,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2014,3,15]],"date-time":"2014-03-15T00:00:00Z","timestamp":1394841600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,11]]},"DOI":"10.1007\/s10009-014-0304-7","type":"journal-article","created":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T05:08:26Z","timestamp":1395119306000},"page":"685-711","source":"Crossref","is-referenced-by-count":40,"title":["Techniques for modelling and verifying railway interlockings"],"prefix":"10.1007","volume":"16","author":[{"given":"Phillip","family":"James","sequence":"first","affiliation":[]},{"given":"Faron","family":"Moller","sequence":"additional","affiliation":[]},{"given":"Hoang Nga","family":"Nguyen","sequence":"additional","affiliation":[]},{"given":"Markus","family":"Roggenbach","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,15]]},"reference":[{"key":"304_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. CUP, Cambridge (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"304_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B, chapter 17-Train System. CUP, Cambridge (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"304_CR3","doi-asserted-by":"crossref","unstructured":"Antoni, M.: Practical formal validation method for interlocking or automated systems. In: 3rd International Workshop on Dependable Control of Discrete Systems (DCDS), 2011, pp. ix\u2013x (2011)","DOI":"10.1109\/DCDS.2011.5970308"},{"key":"304_CR4","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, D.: Dynamics of railway nets: on an interface between automatic control and software engineering. Elsevier. In: CTS (2003)","DOI":"10.1016\/S1474-6670(17)32424-2"},{"key":"304_CR5","doi-asserted-by":"crossref","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: CAV, volume 7358 of LNCS, pp. 378\u2013393. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_29"},{"key":"304_CR6","doi-asserted-by":"crossref","unstructured":"Fantechi, A., Gnesi, S.: On the adoption of model checking in safety-related software industry. In: Computer Safety, Reliability, and Security, pp. 383\u2013396 (2011)","DOI":"10.1007\/978-3-642-24270-0_28"},{"key":"304_CR7","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. FORMS\/FORMAT 2010, 107\u2013115 (2011)","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"304_CR8","unstructured":"Fowler, M.: Domain Specific Languages. Addison-Wesley, Reading (2010)"},{"key":"304_CR9","doi-asserted-by":"crossref","unstructured":"Haxthausen, A.E.: Automated generation of safety requirements from railway interlocking tables. In: ISoLA (2), volume 7610 of LNCS, pp. 261\u2013275. Springer (2012)","DOI":"10.1007\/978-3-642-34032-1_25"},{"issue":"8","key":"304_CR10","doi-asserted-by":"crossref","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":"304_CR11","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"304_CR12","doi-asserted-by":"crossref","unstructured":"Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways-an approach in Timed CSP. In: IFM, pp. 54\u201368 (2012)","DOI":"10.1007\/978-3-642-30729-4_5"},{"key":"304_CR13","unstructured":"Jacquart, R. (ed.): IFIP 18th World Computer Congress, Topical Sessions, chapter TRain: The Railway Domain-A Grand Challenge. Kluwer, Dordrecht (2004)"},{"key":"304_CR14","unstructured":"James, P., Beckmann, A., Roggenbach, M.: Using domain specific languages to support verification in the railway domain. In: Proceedings of HVC\u201912: Eighth Haifa Verification Conference, LNCS. Springer (to appear)"},{"key":"304_CR15","doi-asserted-by":"crossref","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H. : On Modelling and Verifying Railway Interlockings: Tracking Train Lengths. Technical Report CS-13-03, University of Surrey, Department of Computing (2013)","DOI":"10.1016\/j.scico.2014.04.005"},{"key":"304_CR16","unstructured":"James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based modelchecking. ECEASST, 35 (2010)"},{"key":"304_CR17","doi-asserted-by":"crossref","unstructured":"James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S.: OnTrack: an open tooling environment for railway verification. In: Proceedings of NFM\u201913: Fifth NASA Formal Methods Symposium (2013)","DOI":"10.1007\/978-3-642-38088-4_30"},{"key":"304_CR18","unstructured":"Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlockings. Electron. Notes Theor. Comput. Sci. 250, 19\u201331 (2009)"},{"issue":"2","key":"304_CR19","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"6","key":"304_CR20","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1007\/s00165-010-0172-1","volume":"23","author":"M Leuschel","year":"2011","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Asp. Comput. 23(6), 683\u2013709 (2011)","journal-title":"Formal Asp. Comput."},{"key":"304_CR21","doi-asserted-by":"crossref","unstructured":"Mernik, M., Heering, J., Sloane, A.M.: When and how to develop domain-specific languages. ACM Comput. Surv., 37(4) (2005)","DOI":"10.1145\/1118890.1118892"},{"key":"304_CR22","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M.: Covering for CSP. Swansea University, Technical report (2013)"},{"key":"304_CR23","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Combining Event-Based and State-Based Modelling for Railway Verification. Technical Report CS-12-02, University of Surrey (2012)"},{"key":"304_CR24","doi-asserted-by":"crossref","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP $$\\parallel $$ \u2016 B. In: Proceedings of HVC\u201912: Eighth Haifa Verification Conference, p. 16 (2012) (to appear in Springer Lecture Notes in Computer Science)","DOI":"10.1007\/978-3-642-39611-3_20"},{"key":"304_CR25","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Railway modelling in CSP $$\\parallel $$ \u2016 B: The double junction case study. Electron. Commun. EASST, 53, 15 (2012)"},{"key":"304_CR26","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Using ProB and CSP $$\\parallel $$ \u2016 B for railway modelling. In: Proceedings of IFM\u201912 and ABZ 2012 Posters and Tool demos session, pp. 31\u201335 (2012)"},{"key":"304_CR27","doi-asserted-by":"crossref","unstructured":"Morgan. C.C.: Of wp and CSP. In: Beauty is Our Business: A Birthday Salute to Edsger J. Dijkstra, pp. 319\u2013326. Springer (1990)","DOI":"10.1007\/978-1-4612-4476-9_37"},{"key":"304_CR28","doi-asserted-by":"crossref","unstructured":"Morley, M.J.: Safety in railway signalling data: a behavioural analysis. In: HOLTPA, pp. 464\u2013474. Springer (1993)","DOI":"10.1007\/3-540-57826-9_156"},{"key":"304_CR29","unstructured":"National Electronic Sectional Appendix. http:\/\/www.networkrail.co.uk\/aspx\/10563.aspx . Accessed: 01\/05\/2013"},{"key":"304_CR30","unstructured":"Nock, O.-S.: Railway Signalling. IRSE (1980)"},{"key":"304_CR31","unstructured":"Office of Rail Regulations. Estimates of station usage 2011\/12 report. (2013). http:\/\/www.rail-reg.gov.uk\/server\/show\/nav.1529"},{"key":"304_CR32","unstructured":"The ProB animator and model checker (ProB 1.3.6-final). (2013). http:\/\/www.stups.uni-duesseldorf.de\/ProB . Accessed: 01\/05\/2013"},{"key":"304_CR33","doi-asserted-by":"crossref","unstructured":"Sabatier, D., Burdy, L., Requet, A., Gu\u00e9ry, J.: Formal proofs for the NYCT line 7 (flushing) modernization project. In: ABZ, pp. 369\u2013372 (2012)","DOI":"10.1007\/978-3-642-30885-7_34"},{"issue":"4","key":"304_CR34","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"S Schneider","year":"2005","unstructured":"Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Asp. Comput. 17(4), 390\u2013422 (2005)","journal-title":"Formal Asp. Comput."},{"key":"304_CR35","unstructured":"Simpson, A., Woodcock, J., Davies, J.: The mechanical verification of solid-state interlocking geographic data. In: Formal Methods Pacific 97. Springer (1997)"},{"key":"304_CR36","unstructured":"UIC: The International Union of Railways. ETCS reference documents. (2013). http:\/\/www.uic.org . Accessed: 01\/05\/2013"},{"key":"304_CR37","unstructured":"Winter, K.: Model checking railway interlocking systems. Aust. Comput. Sci. Commun. 24(1) (2002)"},{"key":"304_CR38","unstructured":"Winter, K., Robinson, N.: Modelling large railway interlockings and model checking small ones. In: Proceedings of the 26th Australasian Computer Science Conference-Volume 16, pp. 309\u2013316. Australian Computer Society Inc, (2003)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0304-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0304-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0304-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,11]],"date-time":"2023-07-11T07:28:01Z","timestamp":1689060481000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0304-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,15]]},"references-count":38,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,11]]}},"alternative-id":["304"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0304-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,15]]}}}