{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T22:39:08Z","timestamp":1770331148379,"version":"3.49.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319339504","type":"print"},{"value":"9783319339511","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33951-1_10","type":"book-chapter","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T05:21:26Z","timestamp":1465881686000},"page":"134-149","source":"Crossref","is-referenced-by-count":34,"title":["Verification of Railway Interlocking - Compositional Approach with OCRA"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Limbr\u00e9e","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Quentin","family":"Cappart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"Pecheur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,15]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Antoni, M., Ammad, N.: Formal Validation Method and Tools for French Computorized Railway Interlocking Systems, pp. 1\u201310, June 2008","DOI":"10.1049\/ic:20080313"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Busard, S., Cappart, Q., Limbr\u00e9e, C., Pecheur, C., Schaus, P.: Verification of railway interlocking systems. In: Proceedings 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015, Oslo, Norway, June 22, 2015, pp. 19\u201331 (2015). http:\/\/dx.doi.org\/10.4204\/EPTCS.184.2","DOI":"10.4204\/EPTCS.184.2"},{"key":"10_CR4","unstructured":"Cappart, Q., Limbr\u00e9e, C., Schaus, P., Legay, A.: Verification by discrete simulation of interlocking systems. In: Proceedings of the 29th Annual European Simulation and Modelling Conference, EUROSIS, October 2015"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/s001650050022","volume":"10","author":"A Cimatti","year":"1998","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Formal Aspects Comput. 10, 361\u2013380 (1998). doi: 10.1007\/s001650050022","journal-title":"Formal Aspects Comput."},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., 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":"10_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: A tool for checking the refinement of temporal contracts. In: ASE, pp. 702\u2013705 (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"key":"10_CR11","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: Ocra: Othello Contracts Refinement Analysis Versions 1,3. FBK (2015)"},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333\u2013348 (2015)","journal-title":"Sci. Comput. Program."},{"key":"10_CR13","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: FMCAD, pp. 52\u201359. IEEE (2012)"},{"key":"10_CR14","unstructured":"Claessen, K., Sorensson, N.: A liveness checking algorithm that counts. In: Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22\u201325, 2012, pp. 52\u201359 (2012). http:\/\/ieeexplore.ieee.org\/xpl\/articleDetails.jsp?arnumber=6462555"},{"key":"10_CR15","volume-title":"Model Checking","author":"JEM Clarke","year":"1999","unstructured":"Clarke, J.E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"10_CR16","unstructured":"Duggan, P., Bor\u00e4lv, A.: Mathematical proof in an automated environment for railway interlockings. IRSE News Issue 217, Institution of Railway Signal Engineers, 2\u20136 December 2015. www.irse.org"},{"key":"10_CR17","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":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1007\/11813040_35","volume-title":"FM 2006: Formal Methods","author":"W Johnston","year":"2006","unstructured":"Johnston, W., Winter, K., van den Berg, L., Strooper, P., Robinson, P.: Model-based variable and transition orderings for efficient symbolic model checking. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 524\u2013540. Springer, Heidelberg (2006)"},{"key":"10_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Sun, P., Collart-Dutilleul, S., Bon, P.: A model pattern of railway interlocking system by Petri nets. In: 2015 International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS), pp. 442\u2013449, June 2015","DOI":"10.1109\/MTITS.2015.7223292"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/978-3-642-05089-3_7","volume-title":"FM 2009: Formal Methods","author":"S Tonetta","year":"2009","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 89\u2013105. Springer, Heidelberg (2009)"},{"key":"10_CR24","series-title":"Communications in Computer and Information Science","first-page":"223","volume-title":"Formal Techniques for Safety-Critical Systems","author":"LH Vu","year":"2015","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 223\u2013238. Springer, Heidelberg (2015). http:\/\/dx.doi.org\/10.1007\/978-3-319-17581-2_15"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-642-34032-1_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","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). http:\/\/dx.doi.org\/10.1007\/978-3-642-34032-1_24"},{"key":"10_CR26","unstructured":"Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Oudshoorn, M. (ed.) Twenty-Fifth Australasian Computer Science Conference (ACSC 2003), pp. 309\u2013316 (2003)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Xu, T., Tang, T., Gao, C., Cai, B.: Logic verification of collision avoidance system in train control systems. In: 2009 IEEE Intelligent Vehicles Symposium, pp. 918\u2013923, June 2009","DOI":"10.1109\/IVS.2009.5164402"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33951-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T14:25:58Z","timestamp":1568039158000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33951-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319339504","9783319339511"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33951-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}