Formal Reliability Analysis using Theorem Proving
Paper and pencil analysis and computer simulations have traditionally
been used in reliability analysis of engineering systems. Formal
methods based techniques provide an accurate and complementary
alternative to these techniques. In this research, we have developed a
formal reliability analysis approach based on higher-order logic
theorem proving.
The formal reliability analysis method is shown in the Figure above. Our proposed approach facilitates verification, computation, reasoning, and documentation of the reliability proofs in the sound environment of the HOL theorem prover. The green boxes below the top dotted line highlight some of the main features of the proposed reliability analysis method. The higher-order logic theories we have developed enable lifetime reliability modeling using single and multiple random variables. We can prove reliability properties of various engineering system configurations such as series, parallel, series-parallel and parallel-series structures.
We have applied the developed theories to the problems in fault modeling, and reliability analysis of electronic systems. Following are selected peer reviewed publications that highlight our work.
[1] N. Abbasi, O. Hasan, S. Tahar, Formal Lifetime Analysis using Theorem Proving, Workshop on Logic, Languages, Information and Computing (WoLLIC), Brasilia, Brazil, July 6-9, 2010,
[2] O. Hasan, S. Tahar, N. Abbasi: Formal Reliability Analysis using Theorem Proving, IEEE Transactions on Computers, Vol. 59, No. 5, May 2010, pp. 579-592.
[3] O. Hasan, N. Abbasi, B. Akbarpour, S. Tahar, and R. Akbarpour: Formal Reasoning about Expectation Properties for Continuous Random Variables; In: A. Cavalcanti and D. Dams (Eds.), Formal Methods, Lecture Notes in Computer Science 5850, Springer Verlag, 2009, pp. 435-450. [Proc. International Symposium on Formal Methods (FM'09) , Eindhoven, The Netherlands, November 2009.]
[4] O. Hasan, N. Abbasi, and S. Tahar: Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays; In: M. Leuschel and H. Wehrheim (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 5423, Springer Verlag, 2009, pp. 277-291. [Proc. International Conference on Integrated Formal Methods (IFM'09), Dosseldorf, Germany, February 2009.]
The formal reliability analysis method is shown in the Figure above. Our proposed approach facilitates verification, computation, reasoning, and documentation of the reliability proofs in the sound environment of the HOL theorem prover. The green boxes below the top dotted line highlight some of the main features of the proposed reliability analysis method. The higher-order logic theories we have developed enable lifetime reliability modeling using single and multiple random variables. We can prove reliability properties of various engineering system configurations such as series, parallel, series-parallel and parallel-series structures.
We have applied the developed theories to the problems in fault modeling, and reliability analysis of electronic systems. Following are selected peer reviewed publications that highlight our work.
[1] N. Abbasi, O. Hasan, S. Tahar, Formal Lifetime Analysis using Theorem Proving, Workshop on Logic, Languages, Information and Computing (WoLLIC), Brasilia, Brazil, July 6-9, 2010,
[2] O. Hasan, S. Tahar, N. Abbasi: Formal Reliability Analysis using Theorem Proving, IEEE Transactions on Computers, Vol. 59, No. 5, May 2010, pp. 579-592.
[3] O. Hasan, N. Abbasi, B. Akbarpour, S. Tahar, and R. Akbarpour: Formal Reasoning about Expectation Properties for Continuous Random Variables; In: A. Cavalcanti and D. Dams (Eds.), Formal Methods, Lecture Notes in Computer Science 5850, Springer Verlag, 2009, pp. 435-450. [Proc. International Symposium on Formal Methods (FM'09) , Eindhoven, The Netherlands, November 2009.]
[4] O. Hasan, N. Abbasi, and S. Tahar: Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays; In: M. Leuschel and H. Wehrheim (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 5423, Springer Verlag, 2009, pp. 277-291. [Proc. International Conference on Integrated Formal Methods (IFM'09), Dosseldorf, Germany, February 2009.]
