{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T18:53:05Z","timestamp":1760122385497},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105567"},{"type":"electronic","value":"9783319105574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10557-4_17","type":"book-chapter","created":{"date-parts":[[2014,8,27]],"date-time":"2014-08-27T08:12:24Z","timestamp":1409127144000},"page":"137-146","source":"Crossref","is-referenced-by-count":4,"title":["Contract-Based Analysis for Verification of Communication-Based Train Control (CBTC) System"],"prefix":"10.1007","author":[{"given":"Marco","family":"Carloni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orlando","family":"Ferrante","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Ferrari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianpaolo","family":"Massaroli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio","family":"Orazzo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ida","family":"Petrone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Velardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-642-33675-1_38","volume-title":"Computer Safety, Reliability, and Security","author":"O. Ferrante","year":"2012","unstructured":"Ferrante, O., Benvenuti, L., Mangeruca, L., Sofronis, C., Ferrari, A.: Parallel NuSMV: A NuSMV Extension for the Verification of Complex Embedded Systems. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP 2012 Workshops. LNCS, vol.\u00a07613, pp. 409\u2013416. Springer, Heidelberg (2012)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Caillaud, B., Passerone, R.: Multi-viewpoint state machines for rich component models. In: Model-Based Design for Embedded Systems. CRC Press (November 2009)","DOI":"10.1201\/9781420067859-c15"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Benvenuti, L., Ferrari, A., Mangeruca, L., Mazzi, E., Passerone, R., Sofronis, C.: A contract-based formalism for the specification of heterogeneous systems. In: Forum on Specification & Design Languages (FDL 2008) (September 2008)","DOI":"10.1109\/FDL.2008.4641436"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Mangeruca, L., Ferrante, O., Ferrari, A.: Formalization and completeness of evolving requirements using Contracts. In: 2013 8th IEEE International Symposium on Industrial Embedded Systems, SIES (2013)","DOI":"10.1109\/SIES.2013.6601484"},{"key":"17_CR5","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.-B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.: Contracts for System Design (2012)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Ferrante, O., Passerone, R., Ferrari, A., Mangeruca, L., Sofronis, C., D\u2019Angelo, M.: Monitor-Based Run-Time Contract Verification of Distributed Systems. In: 9th IEEE International Symposium on Industrial Embedded Systems, SIES, Pisa (2014)","DOI":"10.1109\/SIES.2014.7087332"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-34032-1_23","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"S. Marrone","year":"2012","unstructured":"Marrone, S., Nardone, R., Orazzo, A., Petrone, I., Velardi, L.: Improving Verification Process in Driverless Metro Systems: The MBAT Project. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol.\u00a07610, pp. 231\u2013245. Springer, Heidelberg (2012)"},{"key":"17_CR8","unstructured":"CESAR: CESAR Project, Cost-efficient methods and processes for safety relevant embedded systems, \n                    \n                      http:\/\/www.cesarproject.eu\/\n                    \n                    \n                   (accessed 2012)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-24270-0_27","volume-title":"Computer Safety, Reliability, and Security","author":"G. Bonifacio","year":"2011","unstructured":"Bonifacio, G., Marmo, P., Orazzo, A., Petrone, I., Velardi, L., Venticinque, A.: Improvement of Processes and Methods in Testing Activities for Safety-Critical Embedded Systems. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol.\u00a06894, pp. 369\u2013382. Springer, Heidelberg (2011)"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/11408901_23","volume-title":"Dependable Computing - EDCC 2005","author":"G. Nicola De","year":"2005","unstructured":"De Nicola, G., di Tommaso, P., Rosaria, E., Francesco, F., Pietro, M., Antonio, O.: A Grey-Box Approach to the Functional Testing of Complex Automatic Train Protection Systems. In: Dal Cin, M., Ka\u00e2niche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol.\u00a03463, pp. 305\u2013317. Springer, Heidelberg (2005)"},{"key":"17_CR11","unstructured":"De Nicola, G., di Tommaso, P., Esposito, R., Flammini, F., Marmo, P., Orazzo, A.: ERTMS\/ETCS: Working Principles and Validation. In: Proceedings of the International Conference on Ship Propulsion and Railway Traction Systems, SPRTS 2005, Bologna, Italy, pp. 59\u201368 (2005)"},{"key":"17_CR12","unstructured":"MathWorks In: Simulink - Simulation and Model-Based Design, \n                    \n                      http:\/\/www.mathworks.com\/products\/simulink"},{"key":"17_CR13","unstructured":"di Tommaso, P., Esposito, R., Marmo, P., Orazzo, A.: Hazard Analysis of Complex Distributed Railway Systems. In: Proc. of International Symposium on Reliable Distributed Systems, SRDS 2003, Florence, Italy, pp. 283\u2013292 (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10557-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T13:41:17Z","timestamp":1558964477000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10557-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319105567","9783319105574"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10557-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}