×

An approach for lifetime reliability analysis using theorem proving. (English) Zbl 1277.68216

Summary: Recently proposed formal reliability analysis techniques have overcome the inaccuracies of traditional simulation based techniques but can only handle problems involving discrete random variables. In this paper, we extend the capabilities of existing theorem proving based reliability analysis by formalizing several important statistical properties of continuous random variables like the second moment and the variance. We also formalize commonly used concepts about the reliability theory such as survival, hazard, cumulative hazard and fractile functions. With these extensions, it is now possible to formally reason about important measures of reliability (the probabilities of failure, the failure risks and the mean-time-to failure) associated with the life of a system that operates in an uncertain and harsh environment and is usually continuous in nature. We illustrate the modeling and verification process with the help of examples involving the reliability analysis of essential electronic and electrical system components.

MSC:

68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

ML; Matlab; HOL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Broughton, E., The Bhopal disaster and its aftermath: a review, Environ. Health, 4, 6, 1-6 (2005)
[2] (1986), Rogers Commission report, Report of the Presidential Commission on the Space Shuttle Challenger Accident, vol. 1, Chapter 4, p. 72
[4] Leemis, L. M., Reliability: Probabilistic Models and Statistical Methods, Ascended Ideas (2009)
[5] Cipra, B., How number theory got the best of the pentium chip, Science (N. S.), 267, 5195, 175 (1995)
[6] Bris, Radim, Exact reliability quantification of highly reliable systems with maintenance, Reliab. Eng. Syst. Saf., 95, 12, 1286-1292 (2010)
[7] Mathworks Inc., Matlab (2011)
[8] Kotz, D.; Newport, C.; Gray, R. S.; Liu, J.; Yuan, Y.; Elliott, C., Experimental evaluation of wireless simulation assumptions, (Proceedings of the ACM International Symposium on Modeling, Analysis and Simulation of Wireless and Mobile Systems (2004)), 78-82
[9] Cavin, D.; Sasson, Y.; Schiper, A., On the accuracy of manet simulators, (Proceedings of the ACM International Workshop on Principles of Mobile Computing (2002)), 38-43
[10] Hurd, J., Formal verification of probabilistic algorithms (2002), University of Cambridge: University of Cambridge Cambridge, UK, PhD thesis
[11] Hasan, O., Formal probabilistic analysis using theorem proving (2008), Concordia University: Concordia University Montreal, QC, Canada, PhD thesis
[12] Hasan, O.; Abbasi, N.; Akbarpour, B.; Tahar, S.; Akbarpour, R., Formal reasoning about expectation properties for continuous random variables, (Formal Methods. Formal Methods, Lecture Notes in Comput. Sci., vol. 5850 (2009)), 435-450
[13] Hasan, O.; Tahar, S.; Abbasi, N., Formal reliability analysis using theorem proving, IEEE Trans. Comput., 59, 5, 579-592 (2010) · Zbl 1366.94784
[14] Abbasi, N.; Hasan, O.; Tahar, S., Formal lifetime reliability analysis using continuous random variables, (Logic, Language, Information and Computation. Logic, Language, Information and Computation, Lecture Notes in Comput. Sci., vol. 6188 (2010), Springer), 84-97 · Zbl 1306.90040
[15] Johnson, A. M.; Malek, M., Survey of software tools for evaluating reliability availability and suviceability, ACM Comput. Surv., 20, 4, 227-269 (1998)
[16] Gordon, M. J.C.; Melham, T. F., Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic (1993), Cambridge University Press · Zbl 0779.68007
[17] Kropf, T., Introduction to Formal Hardware Verification (1999), Springer · Zbl 0931.68018
[18] Dean, S., Considerations involved in making system investments for improved service reliability, EEI Bulletin, 6, 491-496 (1938)
[19] Myers, R. H.; Ball, L. W., Reliability Engineering for Electronic Systems (1964), J. Wiley
[23] Institute of Electrical and Electronics Engineers, IEEE standard reliability program for the development and production of electronic systems and equipment, IEEE, 1332 (1998)
[24] Stiffler, J. J.; Bryant, L. A.; Guccione, L., CARE III final report phase I, vols. I and II (November 1979), SRI International, Technical Report NASA Contractor Rep. 159122 and 159123
[25] Nagel, P. M., Software reliability: Repetitive run experimentation and modeling (1982), Boeing Computer Services Co., Technical Report NASA CR-165836
[26] Costes, A.; Doucet, J. E.; Landrault, C.; Laprie, J. C., SURF: A program for dependability evaluation of complex fault-tolerant computing systems, (Digest of the IEEE Annual Symposium on Fault-Tolerant Computing (1981)), 72-78
[27] Frost, D. F.; Poole, K. F.; Haeussler, D. A., RELIANT: A reliability analysis tool for VLSI interconnects, (Proceedings of the IEEE Custom Integrated Circuits Conference (1998)), 27.8/1-27.8/4
[28] Alam, S. M.; Lip, G. C.; Thompson, C. V.; Troxel, D. E., Circuit level reliability analysis of Cu interconnects, (Proceedings of the International Symposium on Quality Electronic Design (2004)), 238-243
[29] Chery, Y.; Hau-Riege, S.; Alam, S.; Troxel, D. E.; Thompson, C. V., A tool for technology-generic circuit-level reliability projections, (Interconnect Focus Center Annual Review (1999))
[30] Lala, J. H., Mark1 - Markov Modeling Package (1983), The Charles Stark Draper Laboratory: The Charles Stark Draper Laboratory Cambridge, MA
[31] Sanders, W. H.; Meyer, J. F., METASAN: A performability evaluation tool based on stochastic activity networks, (Proceedings of the Fall Joint Computer Conference (1986)), 807-816
[32] Goyal, A.; Carter, W. C.; Silva, D. E.; Lavenberg, E.; Trivedi, K. S., The system availability estimator, (Digest of the IEEE Annual Symposium on Fault-Tolerant Computing (1986)), 84-89
[33] Tu, R. H.; Rosenbaum, E.; Chan, W. Y.; Li, C. C.; Minami, E.; Quader, K.; Ko, P. K.; Hu, C., Berkeley reliability tools-bert, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 12, 10, 1524-1534 (1993)
[34] Leucker, M.; Schallhart, C., A brief account of runtime verification, J. Log. Algebr. Program., 78, 5, 293-303 (2009) · Zbl 1192.68433
[35] Clarke, E.; Grumberg, O.; Peled, D., Model Checking (2000), MIT Press
[36] Donatelli, S.; Sproston, J., CSL model checking for the GreatSPN tool, (Computer and Information Sciences. Computer and Information Sciences, Lecture Notes in Comput. Sci., vol. 3280 (2004), Springer), 543-552
[37] Hillston, J., A Compositional Approach to Performance Modelling (1996), Cambridge University Press: Cambridge University Press New York, NY, USA
[38] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Form. Asp. Comput., 6, 102-111 (1994)
[39] Baier, C.; Haverkort, B. R.; Hermanns, H.; Katoen, J.-P., Model-checking algorithms for continuous-time Markov chains, IEEE Trans. Softw. Eng., 29, 6, 524-541 (2003)
[40] Hurd, J.; McIver, A.; Morgan, C., Probabilistic guarded commands mechanized in HOL, Proceedings of the Workshop on Quantitative Aspects of Programming Languages. Proceedings of the Workshop on Quantitative Aspects of Programming Languages, Electron. Notes Theor. Comput. Sci., 112, 95-111 (2005) · Zbl 1272.68258
[41] Duflot, M.; Kwiatkowska, M.; Norman, G.; Parker, D.; Peyronnet, S.; Picaronny, C.; Sproston, J., Practical applications of probabilistic model checking to communication protocols, (FMICS Handbook on Industrial Critical Systems (2010), IEEE Computer Society Press)
[42] Lecca, P.; Priami, C., Cell cycle control in eukaryotes: a biospi model, Proceedings of the Workshop on Concurrent Models in Molecular Biology. Proceedings of the Workshop on Concurrent Models in Molecular Biology, Electron. Notes Theor. Comput. Sci., 180, 3, 51-63 (2007)
[43] Baier, C.; Haverkort, B.; Hermanns, H.; Katoen, J., Model checking algorithms for continuous time Markov chains, IEEE Trans. Softw. Eng., 29, 4, 524-541 (2003)
[44] Rutten, J.; Kwiatkowska, M.; Norman, G.; Parker, D., Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems, CRM Monogr. Ser., vol. 23 (2004), American Mathematical Society
[45] Kwiatkowska, M.; Norman, G.; Parker, D., Quantitative analysis with the probabilistic model checker PRISM, Electron. Notes Theor. Comput. Sci., 153, 2, 5-31 (2005)
[46] Coble, A., Anonymity, information and machine-assisted proof (2009), University of Cambridge: University of Cambridge Cambridge, UK, PhD thesis
[47] Mhamdi, T.; Hasan, O.; Tahar, S., On the formalization of the Lebesgue integration theory in HOL, (Interactive Theorem Proving. Interactive Theorem Proving, Lecture Notes in Comput. Sci., vol. 6172 (2010), Springer), 387-402 · Zbl 1291.68362
[48] Galambos, J., Advanced Probability Theory (1995), Marcel Dekker · Zbl 0841.60001
[49] Papouli, A.; Pillai, S. U., Probability, Random Variables and Stochastic Processes (2002), McGraw-Hill
[50] Hasan, O.; Tahar, S., Formalization of the continuous probability distributions, (Automated Deduction. Automated Deduction, Lecture Notes in Comput. Sci., vol. 4603 (2007), Springer), 3-18 · Zbl 1213.68570
[51] Evans, M.; Hastings, N.; Peacock, B., Triangular distribution, (Statistical Distributions (2000), Wiley: Wiley New York, NY, USA), 187-188, Chapter 40
[52] Harrison, J., Theorem Proving with the Real Numbers (1998), Springer · Zbl 0932.68099
[53] Moschopoulos, P. G., A general procedure for deriving distributions, Commun. Statist. Theoret. Meth., 12, 17, 2005-2015 (1983) · Zbl 0564.62035
[54] Hogg, R. E.; McKean, J. W.; Craig, A. T., Introduction to Mathematical Statistics (2005), Prentice Hall: Prentice Hall Englewood Cliffs, NJ
[55] Montanari, G.; Simoni, L., Aging phenomenology and modeling, IEEE Trans. Electr. Insul., 28, 5, 755-776 (1993)
[56] Simoni, L., Fundamentals of Endurance of Electrical Insulating Materials (1983), CLUEB: CLUEB Bologna, Italy
[57] Vovos, P., Economic system operation considering the cost of wear of cables, IEEE Trans. Power Syst., 26, 2, 642-652 (2011)
[58] Crine, J. P.; Parpal, J. L.; Lessard, G., A model of aging of dielectric extruded cables, (Proceedings of the International Conference on Conduction and Breakdown in Solid Dielectrics (1989)), 347-351
[59] Abbasi, N.; Hasan, O.; Tahar, S., Formalization of Weibull random variable in HOL (October 2010), Department of Electrical and Computer Engineering, Concordia University: Department of Electrical and Computer Engineering, Concordia University Montreal, QC, Canada, Technical report
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.