Abstract
System safety assessments are integral part of system development as indicated by the ARP4754A standard. These activities are usually performed manually and rely on reviews and engineering judgments with limited use of models to support the assessment phase. In this paper we present an application of Model-Based Safety Assessment to the validation of an Aircraft Electrical Power System (EPS). Safety assessment is a fundamental part of the development for aircraft systems and the use of model-based techniques provides an effective method for the formalization and analysis of such complex systems. A toolchain that integrates the Formal Specs Verifier and the xSAP toolsets is presented and results of the application of the toolchain to the EPS use case are shown.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
SAE: ARP4761 Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment, December 1996
Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)
Dutertre, B., Stavridou, V.: Formal requirements analysis of an avionics control system. IEEE Trans. Software Eng. 23, 267–278 (1997)
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)
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)
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)
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–203 (2015)
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–25 (2013)
Peikenkamp, T., Cavallo, A., Valacca, L., Böde, E., Pretzer, M., Hahn, E.M.: Towards a unified model-based safety assessment. In: Górski, J. (ed.) SAFECOMP 2006. LNCS, vol. 4166, pp. 275–288. Springer, Heidelberg (2006). doi:10.1007/11875567_21
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–135. Springer, Heidelberg (2005). doi:10.1007/11563228_10
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–775 (2011)
Güdemann, 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–478. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75101-4_44
Marazza, M., Ferrante, O., Ferrari, A.: Automatic generation of failure scenarios for SoC. In: ERTS2 2014, Tolouse (2014)
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ăsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 518–535. Springer, Cham (2015). doi:10.1007/978-3-319-21690-4_36
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–539. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_31
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–342. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_22
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)
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–40. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_5
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–146. Springer, Cham (2014). doi:10.1007/978-3-319-10557-4_17
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–189. Springer, Cham (2015). doi:10.1007/978-3-319-24249-1_16
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–416. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33675-1_38
Ferrante, O., Ferrari, A., Marazza, M.: An algorithm for the incremental generation of high coverage tests suites. In: 19th IEEE European Test Symposium (2014)
Ferrante, O., Ferrari, A., Marazza, M.: Formal specs verifier ATG: a tool for model-based generation of high coverage test suites. In: ERTS (2016)
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)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Ferrante, O., Di Guglielmo, L., Senni, V., Ferrari, A. (2017). Application of Model-Based Safety Assessment to the Validation of Avionic Electrical Power Systems. In: Bozzano, M., Papadopoulos, Y. (eds) Model-Based Safety and Assessment. IMBSA 2017. Lecture Notes in Computer Science(), vol 10437. Springer, Cham. https://doi.org/10.1007/978-3-319-64119-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-64119-5_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-64118-8
Online ISBN: 978-3-319-64119-5
eBook Packages: Computer ScienceComputer Science (R0)