{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:33:44Z","timestamp":1764873224564},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_29","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"378-393","source":"Crossref","is-referenced-by-count":27,"title":["Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Raffaele","family":"Corvino","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Lazzaro","sequence":"additional","affiliation":[]},{"given":"Iman","family":"Narasamdya","sequence":"additional","affiliation":[]},{"given":"Tiziana","family":"Rizzo","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"Angela","family":"Sanseviero","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Tchaltsev","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"29_CR1","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10817-010-9172-3","volume":"45","author":"D. Angeletti","year":"2010","unstructured":"Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. J. Autom. Reason.\u00a045(4), 397\u2013414 (2010)","journal-title":"J. Autom. Reason."},{"key":"29_CR2","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Art. Int. and Applications, vol.\u00a0185, pp. 825\u2013885. IOS Press (2009)"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"issue":"5-6","key":"29_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"key":"29_CR6","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) FMCAD, pp. 189\u2013197. IEEE (2010)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"29_CR8","unstructured":"Blast-2.7, \n                    \n                      http:\/\/forge.ispras.ru\/projects\/blast"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: Sat-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"issue":"1","key":"29_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0304-3975(00)00090-6","volume":"253","author":"S.V.A. Campos","year":"2001","unstructured":"Campos, S.V.A., Clarke, E.: The verus language: representing time efficiently with bdds. Theor. Comput. Sci.\u00a0253(1), 95\u2013118 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR11","unstructured":"Cavada, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV User Manual v 2.5 (2011), \n                    \n                      http:\/\/nusmv.fbk.eu"},{"issue":"4","key":"29_CR12","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A New Symbolic Model Checker. STTT\u00a02(4), 410\u2013425 (2000)","journal-title":"STTT"},{"issue":"4","key":"29_CR13","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 Asp. Comput.\u00a010(4), 361\u2013380 (1998)","journal-title":"Formal Asp. Comput."},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-22110-1_24","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos \u2013 A Software Model Checker for SystemC. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 310\u2013316. Springer, Heidelberg (2011)"},{"issue":"5","key":"29_CR15","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"29_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"issue":"4","key":"29_CR18","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst.\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"29_CR19","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci.\u00a089(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-24270-0_28","volume-title":"Computer Safety, Reliability, and Security","author":"A. Fantechi","year":"2011","unstructured":"Fantechi, A., Gnesi, S.: On the Adoption of Model Checking in Safety-Related Software Industry. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol.\u00a06894, pp. 383\u2013396. Springer, Heidelberg (2011)"},{"issue":"2","key":"29_CR21","first-page":"42","volume":"2","author":"A. Ferrari","year":"2011","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A., Tempestini, M.: Adoption of model-based testing and abstract interpretation by a railway signalling manufacturer. IJERTCS\u00a02(2), 42\u201361 (2011)","journal-title":"IJERTCS"},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48166-4_10","volume-title":"Software Engineering - ESEC\/FSE \u201999","author":"A. Gargantini","year":"1999","unstructured":"Gargantini, A., Heitmeyer, C.L.: Using Model Checking to Generate Tests from Requirements Specifications. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, pp. 146\u2013162. Springer, Heidelberg (1999)"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"1","key":"29_CR24","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0167-6423(99)00016-7","volume":"36","author":"V. Hartonas-Garmhausen","year":"2000","unstructured":"Hartonas-Garmhausen, V., Campos, S.V.A., Cimatti, A., Clarke, E., Giunchiglia, F.: Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program.\u00a036(1), 53\u201364 (2000)","journal-title":"Sci. Comput. Program."},{"key":"29_CR25","first-page":"78","volume":"65","author":"G.J. Holzmann","year":"2005","unstructured":"Holzmann, G.J.: Software model checking with SPIN. Adv. in Comp.\u00a065, 78\u2013109 (2005)","journal-title":"Adv. in Comp."},{"key":"29_CR26","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s12544-010-0030-5","volume":"2","author":"S. Jabri","year":"2010","unstructured":"Jabri, S., El Koursi, E., Bourdeaudhuy, T., Lemaire, E.: European railway traffic management system validation using UML\/Petri nets modelling strategy. European Transp. Res. Review\u00a02, 113\u2013128 (2010)","journal-title":"European Transp. Res. Review"},{"key":"29_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D.: European Train Control System: A Case Study in Formal Verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 246\u2013265. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:59:55Z","timestamp":1620129595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}