Formal Dependability Analysis using Higher-order-logic Theorem Proving


Dependability is an umbrella concept that subsumes many key properties about a system, including reliability, maintainability, safety, availability, confidentiality, and integrity. Various dependability modeling techniques have been developed to effectively capture the failure characteristics of systems over time. Traditionally, dependability models are analyzed using paper-and-pencil proof methods and computer based simulation tools but their results cannot be trusted due to their inherent inaccuracy limitations. To overcome these limitations, we propose to leverage upon the recent developments in probabilistic analysis support in higher-order-logic theorem proving to conduct accurate and rigorous dependability analysis. This project provides the formalization of two widely used dependability modeling techniques: (i) Reliability Block Diagrams – a graphical technique used to determine the reliability of overall system by utilizing the failure characteristics of individual system components; and (ii) Fault Trees – used for graphically analyzing the conditions and the factors causing an undesired top event, i.e., a critical event, which can cause the whole system failure upon its occurrence. In particular, we present a RBD and FT-based formal dependability analysis framework that has the ability to accurately and rigorously determine the formal reliability, failure, availability and unavailability of safety-critical systems with arbitrary number of components. To illustrate the practical effectiveness of our proposed infrastructure, we present the formal dependability analysis of several real-world safety-critical systems, including smart grids, WSN data transport protocols, satellite solar arrays, virtual data centers, oil and gas pipeline systems and an air traffic management system using the HOL4 theorem prover.



Proposed Framework





  1. W. Ahmed, O. Hasan, S. Tahar and M. S. Hamdi, “Formal Reliability Analysis of Oil and Gas Pipelines”, Journal of Risk and Reliability, SAGE Journals, doi:10.1177/1748006X17694494 (15 pages), 2017

  2. W. Ahmed, O. Hasan, U. Pervez and J. Qadir, “Reliability Modeling and Analysis of Communication Networks”, Journal of Network and Computer Applications, Elsevier, volume 78, pp. 191-215, 2016.

  3. W. Ahmed, O. Hasan and S. Tahar, “Formalization of Reliability Block Diagrams in Higher-order Logic”, Journal of Applied Logic, Elsevier, volume 18, pp. 19-41, 2016.

  4. W. Ahmed, and O. Hasan, “Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach“, Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA-2016), Springer, LNCS 9984, Beijing, China, pp. 264-279.

  5. W. Ahmed, and O. Hasan, “Formal Availability Analysis using Theorem Proving“, 18th International Conference on Formal Engineering Methods (ICFEM-2016), Springer, LNCS 10009, Tokyo, Japan, pp. 226-242.

  6. W. Ahmed, and O. Hasan, “Formal Dependability Modeling and Analysis: A Survey”, Conferences on Intelligent Computer Mathematics (CICM-2016), Springer, LNCS 9791, Bialystok, Poland, pp. 132-147.

  7. W. Ahmed, O. Hasan and S. Tahar, “Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving”, Implementation of Logics (IWIL-2015), volume 40, EPiC Series in Computing, Suva, Fiji, pp. 1-14.

  8. W. Ahmed, O. Hasan and S. Tahar, “Formal Reliability Analysis of Wireless Sensor Network Data Transport Protocols using HOL“,11th International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob-2015), IEEE, Abu Dhabi, UAE, pp. 217-224.

  9. W. Ahmad and O. Hasan, “Towards Formal Fault Tree Analysis using Theorem Proving”, Conferences on Intelligent Computer Mathematics (CICM-2015), Springer, LNCS 9150, Washington, USA, pp. 39-54.

  10. O. Hasan, W. Ahmed, S. Tahar and M. S. Hamdi, “Reliability Block Diagrams based Analysis: A Survey”, International Conference of Numerical Analysis and Applied Maths (ICNAAM-2014), American Institute of Physics, Rhodes, Greece.

  11. W. Ahmed, O. Hasan, S. Tahar and M. S. Hamdi, “Towards the Formal Reliability Analysis of Oil and Gas Pipelines”, Conferences on Intelligent Computer Mathematics (CICM-2014), Springer, LNAI 8543, Coimbra, Portugal, 2014, pp. 30–44.