A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
Dynamic Fault Trees (DFTs) are increasingly being used for modeling the failure behaviors of systems, particularly dynamic behaviors that cannot be captured using conventional combinatorial models. Traditionally, paper and pencil or simulation are used for the analysis of DFTs. While the former can...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2019-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/8845573/ |
| _version_ | 1818350153732456448 |
|---|---|
| author | Yassmeen Elderhalli Osman Hasan Sofiene Tahar |
| author_facet | Yassmeen Elderhalli Osman Hasan Sofiene Tahar |
| author_sort | Yassmeen Elderhalli |
| collection | DOAJ |
| description | Dynamic Fault Trees (DFTs) are increasingly being used for modeling the failure behaviors of systems, particularly dynamic behaviors that cannot be captured using conventional combinatorial models. Traditionally, paper and pencil or simulation are used for the analysis of DFTs. While the former can provide generic expressions for the probability of failure, its results are prone to human errors. The latter method is based on sampling and the results are not guaranteed to be complete. Leveraging upon the expressive and sound nature of higher-order logic (HOL) theorem proving, it has been recently proposed for the analysis of DFTs algebraically. In this paper, we propose a novel methodology for the formal analysis of DFTs, based on the algebraic approach, while capturing both the qualitative and probabilistic aspects using theorem proving. In this paper, we further enrich the DFT library in HOL by providing the formalization of spare gates with a shared spare and the verification details of their probabilistic behavior. To demonstrate the utilization of our methodology, we apply it for the formal analysis of two safety-critical systems, namely, a drive-by-wire system and a cardiac assist system. |
| first_indexed | 2024-12-13T18:17:19Z |
| format | Article |
| id | doaj.art-c10e8a4e3931448b9cd3efc306c38717 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-13T18:17:19Z |
| publishDate | 2019-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-c10e8a4e3931448b9cd3efc306c387172022-12-21T23:35:49ZengIEEEIEEE Access2169-35362019-01-01713617613619210.1109/ACCESS.2019.29428298845573A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem ProvingYassmeen Elderhalli0https://orcid.org/0000-0003-4437-2933Osman Hasan1Sofiene Tahar2Department of Electrical and Computer Engineering, Concordia University, Montréal, QC, CanadaDepartment of Electrical and Computer Engineering, Concordia University, Montréal, QC, CanadaDepartment of Electrical and Computer Engineering, Concordia University, Montréal, QC, CanadaDynamic Fault Trees (DFTs) are increasingly being used for modeling the failure behaviors of systems, particularly dynamic behaviors that cannot be captured using conventional combinatorial models. Traditionally, paper and pencil or simulation are used for the analysis of DFTs. While the former can provide generic expressions for the probability of failure, its results are prone to human errors. The latter method is based on sampling and the results are not guaranteed to be complete. Leveraging upon the expressive and sound nature of higher-order logic (HOL) theorem proving, it has been recently proposed for the analysis of DFTs algebraically. In this paper, we propose a novel methodology for the formal analysis of DFTs, based on the algebraic approach, while capturing both the qualitative and probabilistic aspects using theorem proving. In this paper, we further enrich the DFT library in HOL by providing the formalization of spare gates with a shared spare and the verification details of their probabilistic behavior. To demonstrate the utilization of our methodology, we apply it for the formal analysis of two safety-critical systems, namely, a drive-by-wire system and a cardiac assist system.https://ieeexplore.ieee.org/document/8845573/Dynamic fault treesqualitative analysisquantitative analysishigher-order logictheorem provingHOL4 |
| spellingShingle | Yassmeen Elderhalli Osman Hasan Sofiene Tahar A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving IEEE Access Dynamic fault trees qualitative analysis quantitative analysis higher-order logic theorem proving HOL4 |
| title | A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving |
| title_full | A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving |
| title_fullStr | A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving |
| title_full_unstemmed | A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving |
| title_short | A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving |
| title_sort | methodology for the formal verification of dynamic fault trees using hol theorem proving |
| topic | Dynamic fault trees qualitative analysis quantitative analysis higher-order logic theorem proving HOL4 |
| url | https://ieeexplore.ieee.org/document/8845573/ |
| work_keys_str_mv | AT yassmeenelderhalli amethodologyfortheformalverificationofdynamicfaulttreesusingholtheoremproving AT osmanhasan amethodologyfortheformalverificationofdynamicfaulttreesusingholtheoremproving AT sofienetahar amethodologyfortheformalverificationofdynamicfaulttreesusingholtheoremproving AT yassmeenelderhalli methodologyfortheformalverificationofdynamicfaulttreesusingholtheoremproving AT osmanhasan methodologyfortheformalverificationofdynamicfaulttreesusingholtheoremproving AT sofienetahar methodologyfortheformalverificationofdynamicfaulttreesusingholtheoremproving |