{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T21:13:12Z","timestamp":1767993192986,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_36","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"518-535","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":43,"title":["Formal Design and Safety Analysis of AIR6110 Wheel Brake System"],"prefix":"10.1007","author":[{"given":"M.","family":"Bozzano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Fernandes Pires","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Kimberly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Petri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Robinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"Bittner, B., Bozzano, M., Cavada, R., Cimatti, A., Gario, M., Griggio, A., Mattarei, C., Micheli, A., Zampedri, G.: The xSAP Safety Analysis Platform. ArXiv e-prints (2015)","DOI":"10.1007\/978-3-662-49674-9_31"},{"key":"36_CR2","unstructured":"Bozzano, M., Cimatti, A., Fernandes Pires, A., Jones, D., Kimberly, G., Petri, T., Robinson, R., Tonetta, S.: AIR6110 Wheel Brake System case study. \n                      https:\/\/es.fbk.eu\/projects\/air6110"},{"key":"36_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-319-11936-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"M Bozzano","year":"2014","unstructured":"Bozzano, M., Cimatti, A., Mattarei, C., Tonetta, S.: Formal safety assessment via contract-based design. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 81\u201397. Springer, Heidelberg (2014)"},{"key":"36_CR4","doi-asserted-by":"publisher","DOI":"10.1201\/b10094","volume-title":"Design and Safety Assessment of Critical Systems","author":"M Bozzano","year":"2010","unstructured":"Bozzano, M., Villafiorita, A.: Design and Safety Assessment of Critical Systems. CRC Press (Taylor and Francis), Boca Raton (2010). An Auerbach Book"},{"key":"36_CR5","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":"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":"36_CR6","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., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 702\u2013705 (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-02658-4_17","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2009","unstructured":"Cimatti, A., Roveri, M., Tonetta, S.: Requirements validation for hybrid systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 188\u2013203. Springer, Heidelberg (2009)"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: 38th Euromicro Conference on Software Engineering and Advanced Applications (SEAA), pp. 21\u201328 (2012)","DOI":"10.1109\/SEAA.2012.68"},{"key":"36_CR10","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333\u2013348 (2014)","journal-title":"Sci. Comput. Program."},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Damm, W., Hungar, H., Josko, B., Peikenkamp, T., Stierand, I.: Using contract-based component specifications for virtual integration testing and architecture design. In: Design, Automation and Test in Europe (DATE), pp. 1023\u20131028 (2011)","DOI":"10.1109\/DATE.2011.5763167"},{"key":"36_CR12","unstructured":"ESACS: The ESACS Project. \n                      www.transport-research.info\/web\/projects\/project_details.cfm?ID=2658\n                      \n                    . Accessed 20 May 2015"},{"key":"36_CR13","unstructured":"FAA: F.A.A.: Advisory Circular (AC) 20\u2013174. \n                      http:\/\/www.faa.gov\/documentLibrary\/media\/Advisory_Circular\/AC%2020-174.pdf"},{"key":"36_CR14","unstructured":"FAA: F.A.A.: Advisory Circular (AC) 23\u20131309-1E. \n                      http:\/\/www.faa.gov\/documentLibrary\/media\/Advisory_Circular\/AC%2023.1309-1E.pdf"},{"key":"36_CR15","unstructured":"FAA: F.A.A.: Advisory Circular (AC) 25.1309-1A. \n                      http:\/\/rgl.faa.gov\/Regulatory_and_Guidance_Library\/rgAdvisoryCircular.nsf\/list\/AC%2025.1309-1A\/$FILE\/AC25.1309-1A.pdf\n                      \n                     (1988)"},{"key":"36_CR16","unstructured":"FBK: nuXmv: a new eXtended model verifier. \n                      https:\/\/nuxmv.fbk.eu"},{"key":"36_CR17","unstructured":"FBK: OCRA: A tool for Contract-Based Analysis. \n                      https:\/\/ocra.fbk.eu"},{"key":"36_CR18","unstructured":"FBK: xSAP: eXtended Safety Analysis Platform. \n                      https:\/\/xsap.fbk.eu"},{"key":"36_CR19","unstructured":"ISAAC: The ISAAC Project. \n                      http:\/\/ec.europa.eu\/research\/transport\/projects\/items\/isaac_en.htm\n                      \n                    . Accessed 20 May 2015"},{"key":"36_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/11563228_10","volume-title":"Computer Safety, Reliability, and Security","author":"A Joshi","year":"2005","unstructured":"Joshi, A., Heimdahl, M.P.E.: Model-based safety analysis of simulink models using SCADE design verifier. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol. 3688, pp. 122\u2013135. Springer, Heidelberg (2005)"},{"key":"36_CR21","unstructured":"Joshi, A., Whalen, M., Heimdahl, M.: Model-based safety analysis final report. Technical Report, NASA\/CR-2006-213953, NASA (2006)"},{"key":"36_CR22","unstructured":"MISSA: The MISSA Project. \n                      www.missa-fp7.eu\n                      \n                    . Accessed 20 May 2015"},{"key":"36_CR23","unstructured":"SAE: ARP4761: Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment (1996)"},{"key":"36_CR24","unstructured":"SAE: ARP4754A: Guidelines for Development of Civil Aircraft and Systems (2010)"},{"key":"36_CR25","unstructured":"SAE: AIR6110: Contiguous Aircraft\/System Development Process Example (2011)"},{"key":"36_CR26","unstructured":"Vesely, W., Stamatelatos, M., Dugan, J., Fragola, J., Minarick III, J., Railsback, J.: Fault tree handbook with aerospace applications. Technical report, NASA (2002)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:10:32Z","timestamp":1563826232000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}