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.

## Publications

[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].

## Source Code

**Thesis**

**Journal Papers**

[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**

[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**

[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].

**HOL Scripts**

**Theories in PDF format**

**Multiprocessor Systems**

**Drive-by-wire System**

**Cardiac Assist System**