{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:41:53Z","timestamp":1743021713262,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319054155"},{"type":"electronic","value":"9783319054162"}],"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-05416-2_13","type":"book-chapter","created":{"date-parts":[[2014,4,5]],"date-time":"2014-04-05T05:41:09Z","timestamp":1396676469000},"page":"195-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Cloud-Enabled Refinement Checking of Railway Signalling Interlockings"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Simpson","sequence":"first","affiliation":[]},{"given":"Jaco","family":"Jacobs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,6]]},"reference":[{"key":"13_CR1","series-title":"LNCS","first-page":"582","volume-title":"FME 1994","author":"KM Hansen","year":"1994","unstructured":"Hansen, K.M.: Validation of a railway interlocking model. In: Naftalin, M., Denvir, T., Bertran, M. (eds.) FME 1994. LNCS, vol. 873, pp. 582\u2013601. Springer, Heidelberg (1994)"},{"key":"13_CR2","series-title":"LNCS","first-page":"465","volume-title":"HUG 1993","author":"MJ Morley","year":"1994","unstructured":"Morley, M.J.: Safety in railway signalling data: a behavioural analysis. In: Joyce, J., Seger, C. (eds.) HUG 1993. LNCS, vol. 780, pp. 465\u2013474. Springer, Heidelberg (1994)"},{"issue":"8","key":"13_CR3","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."},{"issue":"2","key":"13_CR4","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2009.08.015","volume":"250","author":"K Kanso","year":"2009","unstructured":"Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlocking systems. Electron. Notes Theoret. Comput. Sci. 250(2), 19\u201331 (2009)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"13_CR5","unstructured":"James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. In: Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010), Electronic Communication of the European Association of Software, Science and Technology, vol. 35 (2010)"},{"issue":"2","key":"13_CR6","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00165-009-0143-6","volume":"23","author":"AE Haxthausen","year":"2011","unstructured":"Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Form. Asp. Comput. 23(2), 191\u2013219 (2011)","journal-title":"Form. Asp. Comput."},{"key":"13_CR7","first-page":"63","volume-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications","author":"A Fantechi","year":"2013","unstructured":"Fantechi, A., Fokkink, W., Morzenti, A.: Some trends in formal methods applications to railway signalling. In: Gnesi, S., Margaria, T. (eds.) Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 63\u201382. Wiley, Hoboken (2013)"},{"key":"13_CR8","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, N.: A story about formal methods adoption by a railway signaling manufacturer. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 179\u2013189. Springer, Heidelberg (2006)"},{"key":"13_CR9","unstructured":"Winter, K., Robinson, N.J.: Modelling large interlocking systems and model checking small ones. In: Oudshoorn, M. (ed.) Proceedings of the 26th Australasian Computer Science Conference (ACSC 2003), Australian Computer Science, Communications, vol. 16, pp. 309\u2013316 (2003)"},{"key":"13_CR10","unstructured":"Simpson, A.C., Woodcock, J.C.P., Davies, J.W.M.: The mechanical verification of solid state interlocking geographic data. In: Groves, L., Reeves, S. (eds.) Proceedings of Formal Methods Pacific 1997, pp. 223\u2013242. Springer, Wellington (1997)"},{"key":"13_CR11","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, London (1985)"},{"key":"13_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, London (2010)"},{"key":"13_CR13","volume-title":"A Classical Mind: Essays in Honour of C.A.R. Hoare","author":"AW Roscoe","year":"1994","unstructured":"Roscoe, A.W.: Model checking CSP. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall, London (1994)"},{"key":"13_CR14","series-title":"LNCS","first-page":"133","volume-title":"TACAS 1995","author":"AW Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check $$10^{20}$$ dining philosophers for deadlock. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133\u2013152. Springer, Heidelberg (1995)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Nurmi, D., Wolski, R., Grzegorczyk, C., Obertelli, G., Soman, S., Youseff, L., Zagorodnov, D.: The eucalyptus open-source cloud-computing system. In: Proceedings of the 9th IEEE\/ACM International Symposium on Cluster Computing and the Grid (CCGRID 2009), pp. 124\u2013131 (2009)","DOI":"10.1109\/CCGRID.2009.93"},{"key":"13_CR16","series-title":"LNCS","first-page":"281","volume-title":"NSF-SERC 1985","author":"SD Brookes","year":"1985","unstructured":"Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating processes. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) NSF-SERC 1985. LNCS, vol. 197, pp. 281\u2013305. Springer, Heidelberg (1985)"},{"key":"13_CR17","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, London (1997)"},{"key":"13_CR18","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-642-14261-1_11","volume-title":"Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 (FORMS\/FORMAT 2010)","author":"A Ferrari","year":"2011","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 (FORMS\/FORMAT 2010), pp. 107\u2013115. Springer, Heidelberg (2011)"},{"issue":"3","key":"13_CR19","first-page":"148","volume":"134","author":"A Cribbens","year":"1987","unstructured":"Cribbens, A.: Solid state interlocking (SSI): an integrated electronic signalling system for mainline railways. IEE Proc. 134(3), 148\u2013158 (1987)","journal-title":"IEE Proc."},{"key":"13_CR20","unstructured":"British Rail Research: SSI data preparation guide. Published by British Railways Board. ELS-DOC-3080, Issue K of SSI8003-INT and supplements (1990)"},{"key":"13_CR21","unstructured":"Simpson, A.C.: Safety through security. DPhil thesis, Oxford University Computing Laboratory (1996)"},{"key":"13_CR22","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)"},{"key":"13_CR23","series-title":"LNCS","first-page":"22","volume-title":"ATVA 2009","author":"AW Roscoe","year":"2009","unstructured":"Roscoe, A.W., Armstrong, P.J., Pragyesh, : Local Search in Model Checking. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 22\u201338. Springer, Heidelberg (2009)"},{"key":"13_CR24","unstructured":"Goldsmith, M.H., Martin, J.M.R.: The parallelisation of FDR. In: Proceedings of Workshop on Parallel and Distributed Model Checking (PDMC 2002) (2002)"},{"issue":"1\u20132","key":"13_CR25","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s00165-008-0074-7","volume":"21","author":"L Freitas","year":"2009","unstructured":"Freitas, L., Woodcock, J.C.P.: FDR explorer. Form. Asp. Comput. 21(1\u20132), 133\u2013154 (2009)","journal-title":"Form. Asp. Comput."}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05416-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T00:41:56Z","timestamp":1676853716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05416-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319054155","9783319054162"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05416-2_13","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"6 April 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}