{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T20:10:06Z","timestamp":1750795806141,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319641188"},{"type":"electronic","value":"9783319641195"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-64119-5_16","type":"book-chapter","created":{"date-parts":[[2017,8,1]],"date-time":"2017-08-01T13:05:09Z","timestamp":1501592709000},"page":"243-254","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Application of Model-Based Safety Assessment to the Validation of Avionic Electrical Power Systems"],"prefix":"10.1007","author":[{"given":"Orlando","family":"Ferrante","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Di Guglielmo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valerio","family":"Senni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Ferrari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,2]]},"reference":[{"key":"16_CR1","unstructured":"SAE: ARP4761 Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment, December 1996"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1109\/32.588520","volume":"23","author":"B Dutertre","year":"1997","unstructured":"Dutertre, B., Stavridou, V.: Formal requirements analysis of an avionics control system. IEEE Trans. Software Eng. 23, 267\u2013278 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Hamilton, D., Covington, R., Kelly, J., Kirkwood, C., Thomas, M., Flora-Holmquist, A.R., Staskauskas, M.G., Miller, S.P., Srivas, M., Cleland, G., MacKenzie, D.: Experiences in applying formal methods to the analysis of software and system requirements. In: Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, p. 30. IEEE Computer Society, Washington, D.C. (1995)","DOI":"10.1109\/WIFT.1995.515477"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Ferrante, O., Scholte, E., Pinello, C., Ferrari, A., Mangeruca, L., Liu, C., Sofronis, C.: A methodology for increasing the efficiency and coverage of model checking and its application to aerospace systems. In: SAE ASTC Conference, Hartford (2016)","DOI":"10.4271\/2016-01-2053"},{"key":"16_CR6","unstructured":"Xu, H., Oszay, N., Murray, R.: A domain-specific language for reactive control protocols for aircraft electric power systems. In: Hybrid Systems Computation and Control (HSCC) (2013)"},{"issue":"2","key":"16_CR7","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/TCNS.2015.2401174","volume":"2","author":"H Xu","year":"2015","unstructured":"Xu, H., Topcu, U., Murray, R.: Specification and synthesis of reactive protocols for aircraft electric power distribution. IEEE Trans. Control Netw. Syst. 2(2), 193\u2013203 (2015)","journal-title":"IEEE Trans. Control Netw. Syst."},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/ACCESS.2013.2295764","volume":"2","author":"P Nuzzo","year":"2013","unstructured":"Nuzzo, P., Xu, H., Ozay, N., Finn, J., Sangiovanni-Vincentelli, A., Murray, R., Donze, A., Seshia, S.A.: Contract-based methodology for aircraft electric power system design. IEEE Access 2, 1\u201325 (2013)","journal-title":"IEEE Access"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/11875567_21","volume-title":"Computer Safety, Reliability, and Security","author":"T Peikenkamp","year":"2006","unstructured":"Peikenkamp, T., Cavallo, A., Valacca, L., B\u00f6de, E., Pretzer, M., Hahn, E.M.: Towards a unified model-based safety assessment. In: G\u00f3rski, J. (ed.) SAFECOMP 2006. LNCS, vol. 4166, pp. 275\u2013288. Springer, Heidelberg (2006). doi: 10.1007\/11875567_21"},{"key":"16_CR10","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). doi: 10.1007\/11563228_10"},{"issue":"5","key":"16_CR11","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. Comput. J. 54(5), 754\u2013775 (2011)","journal-title":"Comput. J."},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-75101-4_44","volume-title":"Computer Safety, Reliability, and Security","author":"M G\u00fcdemann","year":"2007","unstructured":"G\u00fcdemann, M., Ortmeier, F., Reif, W.: Using deductive cause-consequence analysis (DCCA) with SCADE. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol. 4680, pp. 465\u2013478. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75101-4_44"},{"key":"16_CR13","unstructured":"Marazza, M., Ferrante, O., Ferrari, A.: Automatic generation of failure scenarios for SoC. In: ERTS2 2014, Tolouse (2014)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-319-21690-4_36","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., Cimatti, A., Fernandes Pires, A., Jones, D., Kimberly, G., Petri, T., Robinson, R., Tonetta, S.: Formal design and safety analysis of AIR6110 wheel brake system. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 518\u2013535. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_36"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-49674-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Bittner","year":"2016","unstructured":"Bittner, B., Bozzano, M., Cavada, R., Cimatti, A., Gario, M., Griggio, A., Mattarei, C., Micheli, A., Zampedri, G.: The xSAP safety analysis platform. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 533\u2013539. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_31"},{"key":"16_CR16","unstructured":"http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"16_CR17","unstructured":"http:\/\/www.omg.org\/spec\/QVT\/index.htm"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). doi: 10.1007\/978-3-319-08867-9_22"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Ferrante, O., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: BCL: a compositional contract language for embedded systems. In: 19th IEEE International Conference on Emerging Technologies and Factory Automation, Barcelona (2014)","DOI":"10.1109\/ETFA.2014.7005353"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_5"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). doi: 10.1007\/978-3-319-10557-4_17"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-24249-1_16","volume-title":"Computer Safety, Reliability, and Security","author":"M Carloni","year":"2015","unstructured":"Carloni, M., Ferrante, O., Ferrari, A., Massaroli, G., Orazzo, A., Velardi, L.: Contract modeling and verification with FormalSpecs verifier tool-suite - application to Ansaldo STS rapid transit metro system use case. In: Koornneef, F., Gulijk, C. (eds.) SAFECOMP 2015. LNCS, vol. 9338, pp. 178\u2013189. Springer, Cham (2015). doi: 10.1007\/978-3-319-24249-1_16"},{"key":"16_CR23","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. LNCS, vol. 7613, pp. 409\u2013416. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33675-1_38"},{"key":"16_CR24","unstructured":"Ferrante, O., Ferrari, A., Marazza, M.: An algorithm for the incremental generation of high coverage tests suites. In: 19th IEEE European Test Symposium (2014)"},{"key":"16_CR25","unstructured":"Ferrante, O., Ferrari, A., Marazza, M.: Formal specs verifier ATG: a tool for model-based generation of high coverage test suites. In: ERTS (2016)"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Mangeruca, L., Ferrante, O., Ferrari, A.: Formalization and completeness of evolving requirements using contracts. In: 8th IEEE International Symposium on Industrial Embedded Systems (SIES) (2013)","DOI":"10.1109\/SIES.2013.6601484"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Christalin, B., Colledanchise, M., Ogren, P., Murray, R.: Synthesis of reactive control protocols for switch electrical power systems for commercial application with safety specifications. In: IEEE Symposium on Computational Intelligence in Control and Automation (2016)","DOI":"10.1109\/SSCI.2016.7849873"}],"container-title":["Lecture Notes in Computer Science","Model-Based Safety and Assessment"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-64119-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T19:37:55Z","timestamp":1750793875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-64119-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319641188","9783319641195"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-64119-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"2 August 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}