{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:34:51Z","timestamp":1764873291953,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319050317"},{"type":"electronic","value":"9783319050324"}],"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_15","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T09:36:26Z","timestamp":1394184986000},"page":"189-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Verification of Scheme Plans Using CSP$$||$$B"],"prefix":"10.1007","author":[{"given":"Philip","family":"James","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Faron","family":"Moller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hoang Nga","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Roggenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Trumble","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Williams","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"15_CR1","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":"15_CR2","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Using ProB and CSP$$||$$B for railway modelling. In: Proceedings of IFM 2012 and ABZ 2012 Posters and Tool Demos Session, pp. 31\u201335 (2012)"},{"key":"15_CR3","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Railway modelling in CSP$$||$$B: The double junction case study. Electron. Commun. EASST 53 (2012)"},{"key":"15_CR4","series-title":"LNCS","first-page":"193","volume-title":"HVC 2013","author":"F Moller","year":"2013","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP$$||$$B. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2013. LNCS, vol. 7857, pp. 193\u2013208. Springer, Heidelberg (2013)"},{"key":"15_CR5","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 (2013)","DOI":"10.1016\/j.scico.2014.04.005"},{"key":"15_CR6","series-title":"LNCS","first-page":"435","volume-title":"NFM 2013","author":"P James","year":"2013","unstructured":"James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S.: OnTrack: an open tooling environment for railway verification. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 435\u2013440. Springer, Heidelberg (2013)"},{"key":"15_CR7","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Techniques for modelling and verifying railway interlockings. STTT (to appear)"},{"issue":"4","key":"15_CR8","doi-asserted-by":"publisher","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":"15_CR9","unstructured":"Winter, K., Robinson, N.: Modelling large railway interlockings and model checking small ones. In: Proceedings of the 26th Australasian Computer Science Conference, pp. 309\u2013316. Australian Computer Society, Inc. (2003)"},{"key":"15_CR10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"15_CR11","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Morgan, C.: Of wp and CSP. In: Beauty is our business: a birthday salute to E. W. Dijkstra, pp. 319\u2013326 (1990)","DOI":"10.1007\/978-1-4612-4476-9_37"},{"key":"15_CR13","unstructured":"ProB: The ProB animator and model checker (ProB 1.3.6-final). http:\/\/www.stups.uni-duesseldorf.de\/ProB. Accessed 1 May 2013"},{"key":"15_CR14","volume-title":"Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit","author":"RC Gronback","year":"2009","unstructured":"Gronback, R.C.: Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit. Addison-Wesley Professional, Upper Saddle River (2009)"},{"key":"15_CR15","unstructured":"Kolovos, D., Rose, L., Paige, R., Garc\u00eda-Dom\u00ednguez, A.: The Epsilon Book. The Eclipse Foundation (2012)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, D.: Formal software techniques for railway systems. In: CTS 2000 (2000)","DOI":"10.1016\/S1474-6670(17)38131-4"},{"issue":"6","key":"15_CR17","doi-asserted-by":"publisher","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":"15_CR18","series-title":"LNCS","first-page":"369","volume-title":"ABZ 2012","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., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 369\u2013372. Springer, Heidelberg (2012)"},{"key":"15_CR19","volume-title":"In: Formal Methods Pacific 97","author":"A Simpson","year":"1997","unstructured":"Simpson, A., Woodcock, J., Davies, J.: The mechanical verification of solid-state interlocking geographic data. In: Formal Methods Pacific 97. Springer, Heidelberg (1997)"},{"key":"15_CR20","first-page":"464","volume-title":"In: 6th International Workshop on HOLTPA","author":"MJ Morley","year":"1993","unstructured":"Morley, M.J.: Safety in railway signalling data: a behavioural analysis. In: 6th International Workshop on HOLTPA, pp. 464\u2013474. Springer, Heidelberg (1993)"},{"issue":"8","key":"15_CR21","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":"15_CR22","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS\/FORMAT 2010, pp. 107\u2013115 (2011)","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"15_CR23","first-page":"19","volume":"250","author":"K Kanso","year":"2009","unstructured":"Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlockings. ENTCS 250, 19\u201331 (2009)","journal-title":"ENTCS"},{"key":"15_CR24","unstructured":"James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. Electr. Commun. EASST 35 (2010)"},{"key":"15_CR25","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)"},{"issue":"1","key":"15_CR26","first-page":"303","volume":"24","author":"K Winter","year":"2002","unstructured":"Winter, K.: Model checking railway interlocking systems. Aust. Comput. Sci., Commun. 24(1), 303\u2013310 (2002)","journal-title":"Aust. Comput. Sci., Commun."},{"key":"15_CR27","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS\/FORMAT, pp. 107\u2013115 (2010)","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"15_CR29","series-title":"LNCS","first-page":"246","volume-title":"ISoLA 2012, Part II","author":"K Winter","year":"2012","unstructured":"Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246\u2013260. Springer, Heidelberg (2012)"},{"key":"15_CR30","series-title":"LNCS","first-page":"261","volume-title":"ISoLA 2012, Part II","author":"AE Haxthausen","year":"2012","unstructured":"Haxthausen, A.E.: Automated generation of safety requirements from railway interlocking tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 261\u2013275. Springer, Heidelberg (2012)"},{"issue":"11","key":"15_CR31","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"CL Heitmeyer","year":"1998","unstructured":"Heitmeyer, C.L., Kirby, J., Labaw, B.G., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans. Softw. Eng. 24(11), 927\u2013948 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"15_CR32","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)"}],"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_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T22:48:02Z","timestamp":1676846882000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05032-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319050317","9783319050324"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05032-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}