Formal Dynamic Dependability Analysis using HOL Theorem Proving
Contact: y_elderh@ece.concordia.ca
Dependability analysis is an essential step in the design process of safety-critical systems, where the causes of failure and the probability of failure should be identified at an early stage of the system design process. The dynamic failure characteristics of real-world-systems are usually captured by various dynamic dependability models, such as dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs). In order to conduct the formal dependability analysis of systems that exhibit dynamic failure behaviors, these models need to be captured formally, where their structures, operators and properties are properly formalized. In this project, we formalize the mathematical foundations of DFT algebra, which allows conducting both the qualitative and quantitavie analysis within higher-order logic theorem proving. In addition, we propose a new DRBD algera and provide its formalized operators and mathematical reliability expressions. Furthermore, we formally verify the relationship between DFT and DRBD algebras, which allows the formal analysis of both dependability models using the HOL4 theorem prover.
[2] Y. Elderhalli, W. Ahmad, O. Hasan, and S. Tahar. Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving [web page], Journal of Applied Logics, Vol. 6, No. 3, May 2019, pp. 467-509.
[2] Y. Elderhalli, O. Hasan, and S. Tahar. A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams [web page], In: Y. Ait-Ameur and S. Qin (Eds.), International Conference on Formal Engineering Methods, Lecture Notes in Computer Science 11852, Springer, Cham, 2019, pp. 253-269. [Proc. International Conference on Formal Engineering Methods (ICFEM 19), Shenzhen, China, November 2019]
[3] Y. Elderhalli, M. Volk, O. Hasan, J.P. Katoen and S. Tahar: Formal Verification of Rewriting Rules for Dynamic Fault Trees [web page], In: Ölveczky P., Salaün G. (Eds.), Software Engineering and Formal Methods, Lecture Notes in Computer Science 11724, Springer, Cham, 2019, pp. 513-531. [Proc. Software Engineering and Formal Methods (SEFM 19), Oslo, Norway, September 2019]
[4] Y. Elderhalli, O. Hasan and S. Tahar. Using Machine Learning to Minimize User Intervention in Theorem Proving based Dynamic Fault Tree Analysis; Proc. Conference on Artificial Intelligence and Theorem Proving, Proc. Conference on Artificial Intelligence and Theorem Proving (AITP 19), Obergurgl, Austria, April 2019, pp. 1-2.
[5] Y. Elderhalli, O. Hasan, W. Ahmad and S. Tahar: Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking [web page] In: A. Dutle, C. Munoz, and A. NarkawiczK (Eds.), NASA Formal Methods Symposium, Lecture Notes in Computer Science 10811, Springer Verlag, 2018, pp. 139-156. [Proc. NASA Formal Methods Symposium (NFM 18), Newport News, VA, USA, April 2018]
[2] Y. Elderhalli, O. Hasan, and S. Tahar, Integrating DFT and DRBD Formalizations in HOL4, Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2019. [arxiv].
[3] Y. Elderhalli, O. Hasan, and S. Tahar, A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams [web page], Technical Report, Department of Electrical and Computer Engineering, Concordia University, August 2019. [arxiv].
[4] Y. Elderhalli, W. Ahmad, O. Hasan, and S. Tahar. Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4 [web page], Technical Report, Department of Electrical and Computer Engineering, Concordia University, July 2018. [arxiv].
[5] Y. Elderhalli, O. Hasan, W. Ahmad and S. Tahar. Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking [web page], Technical Report, Department of Electrical and Computer Engineering, Concordia University, December 2017. [arxiv].
Publications
Thesis
Yassmeen Elderhalli, "Dynamic Dependability Analysis using HOL Theorem Proving with Application in Multiprocessor Systems", PhD Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, December 2019.Journal Papers
[1] Y. Elderhalli, O. Hasan, and S. Tahar. A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving [web page], IEEE Access, Vol. 7, No. 1, December 2019, pp. 136176-136192.[2] Y. Elderhalli, W. Ahmad, O. Hasan, and S. Tahar. Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving [web page], Journal of Applied Logics, Vol. 6, No. 3, May 2019, pp. 467-509.
Conference Papers
[1] Y. Elderhalli, O. Hasan, and S. Tahar. A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving;, In: C. Benzmuller and B. Miller (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 12236, Springer, 2020, pp. 105-122. [Proc. Conference on Intelligent Computer Mathematics (CICM'20), Bertinoro, Italy, July 2020][2] Y. Elderhalli, O. Hasan, and S. Tahar. A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams [web page], In: Y. Ait-Ameur and S. Qin (Eds.), International Conference on Formal Engineering Methods, Lecture Notes in Computer Science 11852, Springer, Cham, 2019, pp. 253-269. [Proc. International Conference on Formal Engineering Methods (ICFEM 19), Shenzhen, China, November 2019]
[3] Y. Elderhalli, M. Volk, O. Hasan, J.P. Katoen and S. Tahar: Formal Verification of Rewriting Rules for Dynamic Fault Trees [web page], In: Ölveczky P., Salaün G. (Eds.), Software Engineering and Formal Methods, Lecture Notes in Computer Science 11724, Springer, Cham, 2019, pp. 513-531. [Proc. Software Engineering and Formal Methods (SEFM 19), Oslo, Norway, September 2019]
[4] Y. Elderhalli, O. Hasan and S. Tahar. Using Machine Learning to Minimize User Intervention in Theorem Proving based Dynamic Fault Tree Analysis; Proc. Conference on Artificial Intelligence and Theorem Proving, Proc. Conference on Artificial Intelligence and Theorem Proving (AITP 19), Obergurgl, Austria, April 2019, pp. 1-2.
[5] Y. Elderhalli, O. Hasan, W. Ahmad and S. Tahar: Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking [web page] In: A. Dutle, C. Munoz, and A. NarkawiczK (Eds.), NASA Formal Methods Symposium, Lecture Notes in Computer Science 10811, Springer Verlag, 2018, pp. 139-156. [Proc. NASA Formal Methods Symposium (NFM 18), Newport News, VA, USA, April 2018]
Technical Reports
[1] Y. Elderhalli, O. Hasan, and S. Tahar, Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving [web page], Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2019. [arxiv].[2] Y. Elderhalli, O. Hasan, and S. Tahar, Integrating DFT and DRBD Formalizations in HOL4, Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2019. [arxiv].
[3] Y. Elderhalli, O. Hasan, and S. Tahar, A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams [web page], Technical Report, Department of Electrical and Computer Engineering, Concordia University, August 2019. [arxiv].
[4] Y. Elderhalli, W. Ahmad, O. Hasan, and S. Tahar. Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4 [web page], Technical Report, Department of Electrical and Computer Engineering, Concordia University, July 2018. [arxiv].
[5] Y. Elderhalli, O. Hasan, W. Ahmad and S. Tahar. Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking [web page], Technical Report, Department of Electrical and Computer Engineering, Concordia University, December 2017. [arxiv].
Source Code
HOL Scripts
Theories in PDF format
Applications
Multiprocessor Systems
In multiprocessor networks, the increased number of processing elements requires having a sophisticated interconnection network that must be on one hand efficient with low cost and on the other hand more reliable. We formally model and conduct the dynamic dependability analysis of shuffle-exchange networks (SENs) using DFTs and DRBDs to reason about their behaviors. SENs are multistage interconnection networks (MINs), which are widely used in multiprocessor systems to establish communication between system nodes, including processors, memories and I/O peripherals.
Drive-by-wire System
The drive-by-wire (DBW) system controls the brakes and throttle systems of modern vehicles. This system consists of the following parts: the brakes control unit (BC), the throttle failure (TF), two sensors; the brake sensor (BS) and the throttle sensor (TS), the engine failure (EF) and finally the primary central control (PC) unit with its spare part. We model the spare part of the central control unit as a warm spare. We perform the dynamic dependability analysis using both DFTs and DRBD to verify generic dependability expressions.
Cardiac Assist System
The cardiac assist system (CAS) provides care to patients with heart failure. The system consists of three sub-systems: pumps, motors and CPUs. We formally model and analyze the dependability of CAS using DFTs and DRBDs to reason about the failure and the success.
