Abstract
Dynamic reliability block diagrams (DRBDs) are introduced to overcome the modeling limitations of traditional reliability block diagrams, such as the inability to capture redundant components. However, so far there is no algebraic framework that allows conducting the analysis of a given DRBD based on its structure function. In this paper, we propose a new algebra to formally express the structure function and the reliability of a DRBD with spare constructs based on basic system blocks and newly introduced DRBD operators. We present several simplification properties that allow reducing the structure of a given DRBD. We formalize the proposed algebra in higher-order logic to ensure its soundness, and formally verify its corresponding properties using the HOL4 theorem prover. This includes formally verifying generic reliability expressions of the spare costruct, series, parallel and deeper structures in an extensible manner that allows verifying the reliability of complex systems. Finally, we demonstrate the applicability of this algebra by formally analyzing the reliability of two real-world systems in HOL4.
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
References
Ahmed, W., Hasan, O., Tahar, S.: Formalization of reliability block diagrams in higher-order logic. J. Appl. Logic 18, 19–41 (2016). https://doi.org/10.1016/j.jal.2016.05.007
Altby, A., Majdandzic, D.: Design and Implementation of a Fault-tolerant Drive-by-wire System. Master’s thesis, Chalmers University of Technology, Sweden (2014)
Bistouni, F., Jahanshahi, M.: Analyzing the reliability of shuffle-exchange networks using reliability block diagrams. Reliab. Eng. Syst. Saf. 132, 97–106 (2014). https://doi.org/10.1016/j.ress.2014.07.012
Distefano, S.: System Dependability and Performances: Techniques, Methodologies and Tools. Ph.D. thesis, University of Messina, Italy (2005)
Elderhalli, Y.: DRBD Formal Analysis: HOL4 Script (2019). http://hvg.ece.concordia.ca/code/hol/DRBD/index.php
Elderhalli, Y., Hasan, O., Tahar, S.: A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams. Technical report, Concordia University, Canada (2019). http://arxiv.org/abs/1908.01930
Elderhalli, Y., Ahmad, W., Hasan, O., Tahar, S.: Probabilistic analysis of dynamic fault trees using HOL theorem proving. J. Appl. Logics 2631(3), 469 (2019)
Hasan, O., Ahmed, W., Tahar, S., Hamdi, M.S.: Reliability block diagrams based analysis: a survey. In: Numerical Analysis and Applied Maths, vol. 1648, pp. 850129.1-4 (2015). https://doi.org/10.1063/1.4913184
HOL4: (2019). https://hol-theorem-prover.org/
Merle, G.: Algebraic Modelling of Dynamic Fault Trees, Contribution to Qualitative and Quantitative Analysis. Ph.D. thesis, ENS, France (2010)
Mhamdi, T., Hasan, O., Tahar, S.: Formalization of entropy measures in HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 233–248. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22863-6_18
Qasim, M., Hasan, O., Elleuch, M., Tahar, S.: Formalization of normal random variables in HOL. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 44–59. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_4
Robidoux, R., Xu, H., Xing, L., Zhou, M.: Automated modeling of dynamic reliability block diagrams using colored petri nets. IEEE Trans. Syst. Man Cybern. 40(2), 337 (2010). https://doi.org/10.1109/TSMCA.2009.2034837
Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling. Anal. Tools. Comput. Sci. Rev. 15–16, 29–62 (2015). https://doi.org/10.1016/j.cosrev.2015.03.001
Smith, G.: The Object-Z Specification Language, vol. 1. Springer, New York (2012)
Xu, H., Xing, L.: Formal semantics and verification of dynamic reliability block diagrams for system reliability modeling. In: Software Engineering and Applications, pp. 155–162 (2007)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Elderhalli, Y., Hasan, O., Tahar, S. (2019). A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)