Abstract
Weibull distributions can be used to accurately model failure behaviours of a wide range of critical systems such as on-orbit satellite subsystems. Markov chains have been used extensively to model reliability and performance of engineering systems or applications. However, the exponentially distributed sojourn time of Continuous-Time Markov Chains (CTMCs) can sometimes be unrealistic for satellite systems that exhibit Weibull failures. In this paper, we develop novel semi-Markov models that characterise failure behaviours, based on Weibull failure modes inferred from realistic data sources. We approximate and encode these new models with CTMCs and use the PRISM probabilistic model checker. The key benefit of this integration is that CTMC-based model checking tools allow us to automatically and efficiently verify reliability properties relevant to industrial critical systems.
Y. Lu—This research was partially supported by the EC project “ETCS Advanced Testing and Smart Train Positioning System” (FP7-TRANSPORT-314219). The author Yu Lu was funded by the Scottish Informatics and Computer Science Alliance (SICSA).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
- 2.
Redundancy: the duplication of critical components or functions of a satellite subsystem.
- 3.
Infant mortality: a subsystem fails early due to defects designed into or built into it.
References
Castet, J.F., Saleh, J.H.: Satellite and satellite subsystems reliability: statistical data analysis and modeling. Reliab. Eng. Syst. Safety 94(11), 1718–1728 (2009)
Castet, J.F., Saleh, J.H.: Beyond reliability, multi-state failure analysis of satellite subsystems: a statistical approach. Reliab. Eng. Syst. Safety 95(4), 311–322 (2010)
Feldmann, A., Whitt, W.: Fitting mixtures of exponentials to long-tail distributions to analyze network performance models. Perform. Eval. 31(3–4), 245–279 (1998)
López, G.G.I., Hermanns, H., Katoen, J.-P.: Beyond memoryless distributions: model checking semi-Markov chains. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 57–70. Springer, Heidelberg (2001)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 123–137. Springer, Heidelberg (2000)
Gopinath, K., Elerath, J., Long, D.: Reliability modelling of disk subsystems with probabilistic model checking. Technical report UCSC-SSRC-09-05, University of California, Santa Cruz (2009)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Int. J. Softw. Tools Technol. Transfer 6(2), 128–142 (2004)
Malhotra, M., Reibman, A.: Selecting and implementing phase approximations for semi-Markov models. Commun. Stat.–Stochast. Models 9(4), 473–506 (1993)
Xin, Q., Schwarz, Thomas J. E S.J., Miller, E.L.: Disk infant mortality in large storage systems. In: Proceedings of the 13th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2005), pp. 125–134. IEEE (2005)
Reijsbergen, D., Gilmore, S., Hillston, J.: Patch-based modelling of city-centre bus movement with phase-type distributions. Electron. Notes Theor. Comput. Sci. 310, 157–177 (2015)
Ciobanu, G., Rotaru, A.: Phase-type approximations for non-Markovian systems: a case study. In: Canal, C., Idani, A. (eds.) SEFM 2014 Workshops. LNCS, vol. 8938, pp. 323–334. Springer, Heidelberg (2015)
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Peng, Z., Lu, Y., Miller, A.A., Johnson, C.W., Zhao, T.: Formal specification and quantitative analysis of a constellation of navigation satellites. Qual. Reliab. Eng. Int. 32(2), 345–361 (2014)
Lu, Y., Peng, Z., Miller, A., Zhao, T., Johnson, C.: How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification. Reliab. Eng. Syst. Safety 144, 95–116 (2015)
Peng, Z., Lu, Y., Miller, A.: Uncertainty analysis of phased mission systems with probabilistic timed automata. In: Proceedings of the 7th IEEE International Conference on Prognostics and Health Management (PHM 2016). IEEE (2016)
Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Des. 15(1), 7–48 (1999)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1(1), 162–170 (2000)
Weibull, W.: A statistical distribution function of wide applicability. J. Appl. Mech. 18, 293–297 (1951)
Evans, M., Hastings, N., Peacock, B.: Erlang Distribution. In: Distributions, Statistical (ed.) 3rd edn., pp. 71–73. Wiley, New York (2000)
Bolch, G., Greiner, S., de Meer, H., Trivedi, K.S.: Introduction. In: Queueing networks and markov chains: modeling and performance evaluation with computer science applications. Wiley, New York (1998)
Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Computing Surveys 38(3) (2006)
Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234–248. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Lu, Y., Miller, A.A., Hoffmann, R., Johnson, C.W. (2016). Towards the Automated Verification of Weibull Distributions for System Failure Rates. In: ter Beek, M., Gnesi, S., Knapp, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2016 2016. Lecture Notes in Computer Science(), vol 9933. Springer, Cham. https://doi.org/10.1007/978-3-319-45943-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-45943-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-45942-4
Online ISBN: 978-3-319-45943-1
eBook Packages: Computer ScienceComputer Science (R0)