{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:23:47Z","timestamp":1773840227466,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319119359","type":"print"},{"value":"9783319119366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_7","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T15:11:50Z","timestamp":1414163510000},"page":"81-97","source":"Crossref","is-referenced-by-count":16,"title":["Formal Safety Assessment via Contract-Based Design"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"Cristian","family":"Mattarei","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abdelwahed, S., Karsai, G., Mahadevan, N., Ofsthun, S.C.: Practical Implementation of Diagnosis Systems Using Timed Failure Propagation Graph Models. IEEE T. Instrumentation and Measurement\u00a058(2), 240\u2013247 (2009)","DOI":"10.1109\/TIM.2008.2005958"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge Univ. Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"7_CR3","unstructured":"ARP4754A Guidelines for Development of Civil Aircraft and Systems. SAE (December 2010)"},{"key":"7_CR4","unstructured":"ARP4761 Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. SAE (December 1996)"},{"issue":"4","key":"7_CR5","first-page":"609","volume":"25","author":"R. Banach","year":"2013","unstructured":"Banach, R., Bozzano, M.: The Mechanical Generation of Fault Trees for Reactive Systems via Retrenchment II: Clocked and Feedback Circuits. FAC\u00a025(4), 609\u2013657 (2013)","journal-title":"FAC"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Bate, I., Hawkins, R., McDermid, J.A.: A Contract-based Approach to Designing Safe Systems. In: SCS 2000, pp. 25\u201336 (2003)","DOI":"10.1023\/A:1022920502619"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-92188-2_9","volume-title":"Formal Methods for Components and Objects","author":"A. Benveniste","year":"2008","unstructured":"Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple Viewpoint Contract-Based Specification and Design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 200\u2013225. Springer, Heidelberg (2008)"},{"key":"7_CR8","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.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"5","key":"7_CR9","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M. Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. The Computer Journal\u00a054(5), 754\u2013775 (2011)","journal-title":"The Computer Journal"},{"key":"7_CR10","unstructured":"Bozzano, M., Cimatti, A., Lisagor, O., Mattarei, C., Mover, S., Roveri, M., Tonetta, S.: Symbolic Model Checking and Safety Assessment of Altarica models. ECEASST\u00a046 (2011)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-75596-8_13","volume-title":"Automated Technology for Verification and Analysis","author":"M. Bozzano","year":"2007","unstructured":"Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic fault tree analysis for reactive systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 162\u2013176. Springer, Heidelberg (2007)"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10009-006-0001-2","volume":"9","author":"M. Bozzano","year":"2007","unstructured":"Bozzano, M., Villafiorita, A.: The FSAP\/NuSMV-SA Safety Analysis Platform. STTT\u00a09(1), 5\u201324 (2007)","journal-title":"STTT"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Villafiorita, A.: Design and Safety Assessment of Critical Systems. CRC Press (Taylor and Francis), an Auerbach Book (2010)","DOI":"10.1201\/b10094"},{"key":"7_CR14","unstructured":"Broy, M.: Towards a Theory of Architectural Contracts: - Schemes and Patterns of Assumption\/Promise Based System Specification. In: Software and Systems Safety - Specification and Verification, pp. 33\u201387. IOS Press (2011)"},{"key":"7_CR15","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. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"key":"7_CR16","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.\u00a05643, pp. 188\u2013203. Springer, Heidelberg (2009)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: SEAA, pp. 21\u201328 (2012)","DOI":"10.1109\/SEAA.2012.68"},{"issue":"2","key":"7_CR18","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM TOPLAS"},{"key":"7_CR19","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: DATE, pp. 1023\u20131028 (2011)","DOI":"10.1109\/DATE.2011.5763167"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"McKelvin Jr., M.L., Eirea, G., Pinello, C., Kanajan, S., Sangiovanni-Vincentelli, A.: A formal approach to fault tree synthesis for the analysis of distributed fault tolerant systems. In: EMSOFT, pp. 237\u2013246. ACM (2005)","DOI":"10.1145\/1086228.1086272"},{"key":"7_CR21","unstructured":"The MISSA Project, \n                  \n                    http:\/\/www.missa-fp7.eu"},{"key":"7_CR22","unstructured":"nuXmv: a new eXtended model verifier, \n                  \n                    https:\/\/nuxmv.fbk.eu"},{"key":"7_CR23","unstructured":"Pinello, C., Carloni, L.P., Sangiovanni-Vincentelli, A.: Fault-tolerant deployment of embedded software for cost-sensitive real-time feedback-control applications. In: DATE, p. 21164. IEEE Computer Society (2004)"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (FOCS 1977), pp. 46\u201357. IEEE Computer Society Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR25","unstructured":"Siddiqi, S.A., Huang, J.: Hierarchical Diagnosis of Multiple Faults. In: IJCAI, pp. 581\u2013586 (2007)"},{"key":"7_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","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T04:02:04Z","timestamp":1559016124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}