{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T18:54:23Z","timestamp":1760122463639},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242484"},{"type":"electronic","value":"9783319242491"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24249-1_16","type":"book-chapter","created":{"date-parts":[[2015,9,7]],"date-time":"2015-09-07T11:43:15Z","timestamp":1441626195000},"page":"178-189","source":"Crossref","is-referenced-by-count":3,"title":["Contract Modeling and Verification with FormalSpecs Verifier Tool-Suite - Application to Ansaldo STS Rapid Transit Metro System Use Case"],"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":"Luigi","family":"Velardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,9]]},"reference":[{"key":"16_CR1","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":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-319-10557-4_17","volume-title":"Computer Safety, Reliability, and Security","author":"M Carloni","year":"2014","unstructured":"Carloni, M., Ferrante, O., Ferrari, A., Massaroli, G., Orazzo, A., Petrone, I., Velardi, L.: Contract-Based analysis for verification of communication-based train control (cbtc) system. In: Bondavalli, A., Ceccarelli, A., Ortmeier, F. (eds.) SAFECOMP 2014. LNCS, vol. 8696, pp. 137\u2013146. Springer, Heidelberg (2014)"},{"key":"16_CR3","unstructured":"MBAT: Combined Model-based Analysis and Testing of Embedded Systems, Accessed 2011-2014. \n                      http:\/\/www.mbat-artemis.eu\/home\/"},{"key":"16_CR4","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 Workshops 2012. LNCS, vol. 7613, pp. 409\u2013416. Springer, Heidelberg (2012)"},{"key":"16_CR5","unstructured":"Marazza, M., Ferrante, O., Ferrari, A.: Automatic Generation of Failure Scenarios for SoC., Tolouse, Embedded Real Time Software and Systems (2014)"},{"key":"16_CR6","unstructured":"SPEEDS Consortium In: SPEculative and Exploratory Design in Systems Engineering, Accessed 2010. \n                      https:\/\/speeds.eu.com\/"},{"key":"16_CR7","unstructured":"SPRINT Consortium: D2.1 SPRINT Requirements (2011)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Caillaud, B., Passerone, R.: Multi-viewpoint state machines for rich component models. In: Press, C. (ed.): Model-Based Design for Embedded Systems, November 2009","DOI":"10.1201\/9781420067859-c15"},{"key":"16_CR9","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. Forum on Specification & Design Languages (FDL 2008), September 2008","DOI":"10.1109\/FDL.2008.4641436"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Ferrante, O., Mignogna, A., Sofronis, C., Mangeruca, L., Ferrari, A.: Contract based design chain integration: An automotive domain case study. In: Applied Simulation and Modelling, ACTA Press (2011)","DOI":"10.2316\/P.2011.715-008"},{"key":"16_CR11","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. 3463, pp. 305\u2013317. Springer, Heidelberg (2005)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-30138-7_11","volume-title":"Computer Safety, Reliability, and Security","author":"G Nicola De","year":"2004","unstructured":"De Nicola, G., di Tommaso, P., Esposito, R., Flammini, F., Orazzo, A.: A hybrid testing methodology for railway control systems. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, pp. 116\u2013129. Springer, Heidelberg (2004)"},{"key":"16_CR13","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":"16_CR14","doi-asserted-by":"crossref","unstructured":"Donini, R., Marrone, S., Mazzocca, N., Orazzo, A., Papa, D., Venticinque, S.: Testing complex safety-critical systems in SOA context. In: Proceedings of the 2008 International Conference on Complex, Intelligent and Software Intensive Systems (CISIS), Barcelona, Spain (2008)","DOI":"10.1109\/CISIS.2008.78"},{"key":"16_CR15","unstructured":"MathWorks. In: Simulink - Simulation and Model-Based Design. \n                      http:\/\/www.mathworks.com\/products\/simulink"},{"key":"16_CR16","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. 6894, pp. 369\u2013382. Springer, Heidelberg (2011)"}],"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-24249-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:14Z","timestamp":1559253674000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24249-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242484","9783319242491"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24249-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}