{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T00:20:37Z","timestamp":1783988437932,"version":"3.55.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319986531","type":"print"},{"value":"9783319986548","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99130-6_7","type":"book-chapter","created":{"date-parts":[[2018,8,16]],"date-time":"2018-08-16T08:33:48Z","timestamp":1534408428000},"page":"91-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal Verification of Signalling Programs with SafeCap"],"prefix":"10.1007","author":[{"given":"Alexei","family":"Iliasov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominic","family":"Taylor","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Linas","family":"Laibinis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Romanovsky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,8,17]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11415787_20","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F Badeau","year":"2005","unstructured":"Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334\u2013354. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11415787_20"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM 1999 \u2014 Formal Methods","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., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22"},{"key":"7_CR4","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Proccedings of Boogie 2011, pp. 53\u201364 (2011)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Busard, S., Cappart, Q., Limbr\u00e9e, C., Pecheur, C., Schaus, P.: Verification of railway interlocking systems. In: Proceedings of ESSS 2015, pp. 19\u201331 (2015)","DOI":"10.4204\/EPTCS.184.2"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Cappart, Q., Limbr\u00e9e, C., Schaus, P., Quilbeuf, J., Traonouez, L.-M. Legay, A.: Verification of interlocking systems using statistical model checking. In: Proceedings of HASE - High Assurance Systems Engineering, pp. 61\u201368 (2017)","DOI":"10.1109\/HASE.2017.10"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31424-7_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., et al.: 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). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_29"},{"key":"7_CR8","unstructured":"Department for Transport: RAIB review of the railway industry\u2019s investigation of an irregular signal sequence at Milton Keynes (2008). https:\/\/www.gov.uk\/raib-reports\/review-of-the-railway-industry-s-formal-investigation-of-an-irregular-signal-sequence-at-milton-keynes"},{"key":"7_CR9","unstructured":"Gonschorek, T., Bedau, L., Ortmeier, F.: Automatic model-based verification of railway interlocking systems using model checking. In: Proceedings of ESREL (2018)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-45614-7_12","volume-title":"FME 2002:Formal Methods\u2014Getting IT Right","author":"M Huber","year":"2002","unstructured":"Huber, M., King, S.: Towards an integrated model checker for railway signalling data. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 204\u2013223. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_12"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-40793-2_12","volume-title":"Computer Safety, Reliability, and Security","author":"A Iliasov","year":"2013","unstructured":"Iliasov, A., Lopatkin, I., Romanovsky, A.: The safecap platform for modelling railway safety and capacity. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 130\u2013137. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_12"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-319-08311-7_14","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2014","author":"A Iliasov","year":"2014","unstructured":"Iliasov, A., Lopatkin, I., Romanovsky, A.: Practical formal methods in railways - the safecap approach. In: George, L., Vardanega, T. (eds.) Ada-Europe 2014. LNCS, vol. 8454, pp. 177\u2013192. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08311-7_14"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Iliasov, A., Romanovsky, A.: SafeCap domain language for reasoning about safety and capacity. In: Proceedings of PRDC - Pacific-Rim Dependable Computing, pp. 1\u201310. IEEE (2012)","DOI":"10.1109\/WDTS-RASD.2012.11"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Iliasov, A., Romanovsky, A.B.: Formal analysis of railway signalling data. In: Proceedings of HASE - High Assurance Systems Engineering, pp. 70\u201377 (2016)","DOI":"10.1109\/HASE.2016.44"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-33951-1_9","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"A Iliasov","year":"2016","unstructured":"Iliasov, A., Stankaitis, P., Adjepon-Yamoah, D.: Static verification of railway schema and interlocking design data. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 123\u2013133. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_9"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-05032-4_19","volume-title":"Software Engineering and Formal Methods","author":"P James","year":"2014","unstructured":"James, P.: Verification of solid state interlocking programs. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 253\u2013268. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-05032-4_19"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-33951-1_10","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"C Limbr\u00e9e","year":"2016","unstructured":"Limbr\u00e9e, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of railway interlocking - compositional approach with OCRA. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 134\u2013149. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_10"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-319-47169-3_20","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"HD Macedo","year":"2016","unstructured":"Macedo, H.D., Fantechi, A., Haxthausen, A.E.: Compositional verification of multi-station interlocking systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 279\u2013293. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_20"},{"key":"7_CR20","unstructured":"Morley, M.J.: Safety Assurance in Interlocking Design. PhD thesis, University of Edinburgh (1996)"}],"container-title":["Lecture Notes in Computer Science","Developments in Language Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99130-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T07:28:26Z","timestamp":1571729306000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99130-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319986531","9783319986548"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99130-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}