Abstract
Safety assessment is a well-established process for assuring the safety and reliability of critical (aeronautical) systems. It uses probabilistic (quantitative) analysis to provide precise measures about the safety requirements of a system. Traditionally, quantitative safety assessment uses fault-tree analysis, but certification authorities also allow the use of Markov models. In this paper we propose a strategy for quantitative safety assessment based on the Prism model-checker. Prism models are extracted systematically from a high-level model via the application of translation rules. We illustrate our strategy with a representative system design from the airborne industry.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Serra, P.R.: Safety Assessment of aircraft systems, 2nd edn. (2008)
ARP 4761: Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems, SAE Inc. (November 1996)
Stamatelatos, M., et al.: Fault Tree Handbook with Aerospace Applications. NASA Office of Safety and Mission Assurance, Washington (August 2002)
Mota, A., Gomes, A., Jesus, J., Ferri, F., Watanabe, E.: Evolving a Safe System Design Iteratively. Accepted for publication in Proceedings of SAFECOMP (2010)
Papadopoulos, Y., McDermid, J., Sasse, R., Heiner, G.: Analysis and synthesis of the behaviour of complex programmable electronic systems in conditions of failure. Reliability Engineering & System Safety 71(3), 229–247 (2001)
Alexander, R.D., Kelly, T.P.: Escaping the non-quantitative trap. In: 27th International System Safety Conference, pp. 69–95 (2009)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. ACM SIGMETRICS Performance Evaluation Review 36(4), 40–45 (2009)
Kwiatkowska, M., Norman, G., Parker, D.: Quantitative analysis with the Probabilistic Model Checker PRISM. Electronic Notes in Theoretical Computer Science 153(2), 5–31 (2005)
The MathWorks Inc. Simulink User’s Guide (2008)
McDermid, J.A., Lisagor, O., Pumfrey, D.J.: Towards a Practicable Process for Automated Safety Analysis. In: 24th Int. System Safety Conference, pp. 596–607 (2006)
Joshi, A., Heimdahl, M.P.: 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)
Software considerations in airborne systems and equipment certification. DO-178B, RTCA Inc., Washington D.C. (December 1992)
Kerlund, O.A., et al.: ISAAC, A framework for integrated safety analysis of functional, geometrical and human aspects. In: ERTS (2006)
Papadopoulos, Y., Maruhn, M.: Model-based synthesis of fault trees from Matlab-Simulink models. In: Inter. Conference on Dependable Systems and Networks (2001)
Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: The FSAP/NuSMV-SA safety analysis platform. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 49–62. Springer, Heidelberg (2003)
Haverkort, B.R.: Markovian models for performance and dependability evaluation. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 38–83. Springer, Heidelberg (2001)
Saglimbene, M.S.: Reliability analysis techniques: How they relate to aircraft certification. In: Reliability and Maintainability Symposium, pp. 218–222 (2009)
Grunske, L., Colvin, R., Winter, K.: pFMEA: Probabilistic Model-Checking Support for FMEA. In: 4th Int. Conference on the QEST (2007)
Gomes, A.: Technical Report, http://www.cin.ufpe.br/~ajog/tr.pdf
Siewiorek, D., Swarz, R.: Reliable Computer System: Design and Evaluation, 3rd edn (1998)
Aljazzar, H., et al.: Safety Analysis of an Airbag System Using Probabilistic FMEA and Probabilistic Counterexamples. In: QEST, pp. 299–308 (2009)
Bozzano, M., et al.: The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. In: Proceedings of the 28th Int. Conference on Computer Safety, Reliability and Security, September 15-18 (2009)
Alejandro, D., et al.: An integrated methodology for the dynamic performance and reliability evaluation of fault-tolerant systems. Reliability Engineering & System Safety 93(11), 1628–1649 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gomes, A., Mota, A., Sampaio, A., Ferri, F., Buzzi, J. (2010). Systematic Model-Based Safety Assessment Via Probabilistic Model Checking. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification, and Validation. ISoLA 2010. Lecture Notes in Computer Science, vol 6415. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16558-0_50
Download citation
DOI: https://doi.org/10.1007/978-3-642-16558-0_50
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16557-3
Online ISBN: 978-3-642-16558-0
eBook Packages: Computer ScienceComputer Science (R0)