Elderhalli, Yassmeen 
ORCID: https://orcid.org/0000-0003-4437-2933, Hasan, Osman and Tahar, Sofiène
(2019)
A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving.
IEEE Access, 7
.
pp. 136176-136192.
ISSN 2169-3536
Preview |
Text (application/pdf)
7MBElderhalli-IEEE Access-2019.pdf - Published Version Available under License Creative Commons Attribution. |
Official URL: http://dx.doi.org/10.1109/ACCESS.2019.2942829
Abstract
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.
| Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering |
|---|---|
| Item Type: | Article |
| Refereed: | Yes |
| Authors: | Elderhalli, Yassmeen and Hasan, Osman and Tahar, Sofiène |
| Journal or Publication: | IEEE Access |
| Date: | 2019 |
| Funders: |
|
| Digital Object Identifier (DOI): | 10.1109/ACCESS.2019.2942829 |
| Keywords: | Dynamic fault trees, qualitative analysis, quantitative analysis, higher-order logic, theorem proving, HOL4 |
| ID Code: | 986094 |
| Deposited By: | Krista Alexander |
| Deposited On: | 13 Nov 2019 22:03 |
| Last Modified: | 13 Nov 2019 22:03 |
References:
1. E. Ruijters, M. Stoelinga, "Fault tree analysis: A survey of the state-of-the-art in modeling analysis and tools", Comput. Sci. Rev., vol. 15, pp. 29-62, Mar. 2015.2. M. Stamatelatos, W. Vesely, J. Dugan, J. Fragola, J. Minarick, J. Railsback, Fault Tree Handbook with Aerospace Applications: NASA Office of Safety and Mission Assurance, Washington, DC, USA:NASA, 2002.
3. J. Dugan, S. J. Bavuso, M. A. Boyd, "Fault trees and sequence dependencies", Proc. Annu. Rel. Maintainability Symp., pp. 286-293, Jan. 1990.
4. H. Boudali, P. Crouzen, M. Stoelinga, "Dynamic fault tree analysis using input/output interactive Markov chains", Proc. 37th Annu. IEEE/IFIP Int. Conf. Dependable Syst. Netw. (DSN), pp. 708-717, Jun. 2007.
5. G. Merle, J. M. Roussel, J. J. Lesage, A. Bobbio, "Probabilistic algebraic analysis of fault trees with priority dynamic gates and repeated events", IEEE Trans. Rel., vol. 59, pp. 250-261, Mar. 2010.
6. C. Mooney, Monte Carlo Simulation, Newbury Park, CA, USA:Sage, 1997.
7. L. Pullum, J. Dugan, "Fault tree models for the analysis of complex computer-based systems", Proc. Annu. Rel. Maintainability Symp., pp. 200-207, Jan. 1996.
8. L. Xing, S. Amari, Binary Decision Diagrams and Extensions for System Reliability Analysis, Hoboken, NJ, USA:Wiley, 2015.
9. G. Merle, "Algebraic modelling of dynamic fault trees contribution to qualitative and quantitative analysis", 2010.
10. G. Merle, J.-M. Roussel, J.-J. Lesage, V. Perchet, N. Vayatis, "Quantitative analysis of dynamic fault trees based on the coupling of structure functions and Monte Carlo simulation", Qual. Rel. Eng. Int., vol. 32, no. 1, pp. 7-18, 2016.
11. O. Hasan, S. Tahar, "Formal Verification Methods" in Encyclopedia of Information Science and Technology, Hershey, PA, USA:IGI Global, pp. 7162-7170, 2015.
12. C. Baier, J. Katoen, Principles of Model Checking, Cambridge, MA, USA:MIT Press, 2008.
13. M. J. Gordon, T. F. Melham, Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge, U.K.:Univ. Cambridge Press, 1993.
14. C. Dehnert, S. Junges, J. Katoen, M. Volk, "A storm is coming: A modern probabilistic model checker" in Computer Aided Verification, Cham, Switzerland:Springer, vol. 10472, pp. 592-600, 2017.
15. M. Ghadhab, S. Junges, J. Katoen, M. Kuntz, M. Volk, "Safety analysis for vehicle guidance systems with dynamic fault trees", Rel. Eng. Syst. Saf., vol. 186, pp. 37-50, Jul. 2019.
16. Y. Elderhalli, O. Hasan, W. Ahmad, S. Tahar, "Formal dynamic fault trees analysis using an integration of theorem proving and model checking" in NASA Formal Methods, Cham, Switzerland:Springer, vol. 10811, pp. 139-156, 2018.
17. Y. Elderhalli, W. Ahmad, O. Hasan, S. Tahar, "Probabilistic analysis of dynamic fault trees using HOL theorem proving", J. Appl. Logics, vol. 6, no. 3, pp. 469, 2019.
18. J. Ni, W. Tang, Y. Xing, "A simple algebra for fault tree analysis of static and dynamic systems", IEEE Trans. Rel., vol. 62, no. 4, pp. 846-861, Dec. 2013.
19. A. Altby, D. Majdandzic, "Design and implementation of a fault-tolerant drive-by-wire system", 2014.
20. H. Boudali, P. Crouzen, M. Stoelinga, "A rigorous compositional and extensible framework for dynamic fault tree analysis", IEEE Trans. Dependable Secure Comput., vol. 7, no. 2, pp. 128-143, Apr. 2010.
21. K. J. Sullivan, J. B. Dugan, D. Coppit, "The Galileo fault tree analysis tool", Proc. 29th Annu. Int. Symp. Fault-Tolerant Comput., pp. 232-235, Jun. 1999.
22. F. Arnold, A. Belinfante, F. V. der Berg, D. Guck, M. Stoelinga, "DFTCalc: A tool for efficient fault tree analysis" in Computer Safety Reliability and Security, Cham, Switzerland:Springer, vol. 8153, pp. 293-301, 2013.
23. X. Song, Z. Zhai, P. Zhu, J. Han, "A stochastic computational approach for the analysis of fuzzy systems", IEEE Access, vol. 5, pp. 13465-13477, 2017.
24. D. Codetta-Raiteri, "The conversion of dynamic fault trees to stochastic Petri nets as a case of graph transformation", Electron. Notes Theor. Comput. Sci., vol. 127, no. 2, pp. 45-60, 2005.
25. G. Franceschinis, S. Donatelli, R. Gaeta, "GreatSPN 2.0: Graphical editor and analyzer for timed and stochastic Petri Nets", Proc. Petri Nets, pp. 43, 2000.
26. PRISM, 2019, [online] Available: http://www.prismmodelchecker.org/.
27. M. Volk, S. Junges, J.-P. Katoen, "Fast dynamic fault tree analysis by model checking techniques", IEEE Trans Ind. Informat., vol. 14, no. 1, pp. 370-379, Jan. 2018.
28. J. Hurd, "Formal verification of probabilistic algorithms", 2002.
29. O. Hasan, "Formal probabilistic analysis using theorem proving", 2008.
30. T. Mhamdi, "Information-theoretic analysis using theorem proving", 2012.
31. J. Hòlzl, "Construction and stochastic applications of measure spaces in higher-order logic", 2012.
32. N. Abbasi, O. Hasan, S. Tahar, "Formal lifetime reliability analysis using continuous random variables", Proc. Int. Workshop Logic Lang. Inf. Comput., pp. 84-97, 2010.
33. O. Hasan, S. Tahar, N. Abbasi, "Formal reliability analysis using theorem proving", IEEE Trans. Comput., vol. 59, no. 5, pp. 579-592, May 2010.
34. W. Ahmad, O. Hasan, "Formalization of fault trees in higher-order logic: A deep embedding approach" in Dependable Software Engineering: Theories Tools and Applications, Cham, Switzerland:Springer, vol. 9984, pp. 264-279, 2016.
35. W. Ahmad, O. Hasan, "Towards formal fault tree analysis using theorem proving" in Intelligent Computer Mathematics, Cham, Switzerland:Springer, vol. 9150, pp. 39-54, 2015.
36. HOL4, 2019, [online] Available: https://hol-theorem-prover.org/.
37. Isabelle, 2019, [online] Available: https://isabelle.in.tum.de/.
38. Coq, 2019, [online] Available: https://coq.inria.fr/.
39. T. Mhamdi, O. Hasan, S. Tahar, "On the formalization of the Lebesgue integration theory in HOL" in Interactive Theorem Proving, Cham, Switzerland:Springer, vol. 6172, pp. 387-402, 2010.
40. T. Mhamdi, O. Hasan, S. Tahar, "Formalization of entropy measures in HOL" in Interactive Theorem Proving, Cham, Switzerland:Springer, vol. 6898, pp. 233-248, 2011.
41. M. Qasim, O. Hasan, M. Elleuch, S. Tahar, "Formalization of normal random variables in HOL" in Intelligent Computer Mathematics, Springer, vol. 9791, pp. 44-59, 2016.
42. H. Boudali, J. Bechta Dugan, "A continuous-time Bayesian network reliability modeling and analysis framework", IEEE Trans. Rel., vol. 55, no. 1, pp. 86-97, Mar. 2006.
43. G. Merle, J.-M. Roussel, J.-J. Lesage, "Improving the efficiency of dynamic fault tree analysis by considering gate FDEP as static", Proc. Eur. Saf. Rel. Conf., pp. pp-845, 2010.
44. Y. Elderhalli, O. Hasan, W. Ahmad, S. Tahar, "Dynamic fault trees analysis using an integration of theorem proving and model checking", arXiv:1712.02872, Dec. 2017, [online] Available: https://arxiv.org/abs/1712.02872.
45. G. Merle, J.-M. Roussel, J.-J. Lesage, "Quantitative Analysis of Dynamic Fault Ttrees based on the Structure Function", Qual. Rel. Eng. Int., vol. 30, no. 1, pp. 143-156, 2014.
46. MATLAB 2017a, Natick, MA, USA:The MathWorks, 2017.
47. Y. Elderhalli, DFT Formal Analysis: HOL4 Script, 2019, [online] Available: http://hvg.ece.concordia.ca/code/hol/DFT_method/index.php.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.
Repository Staff Only: item control page
Download Statistics
Download Statistics