Formalization of reliability block diagrams in higher-order logic

DOI10.1016/J.JAL.2016.05.007MaRDI QIDQ334147zbMATH OpenOpenAlexFDO

Authors Waqar Ahmed, Osman Hasan, Sofiène Tahar

Publication date 31 October 2016

Published in Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jal.2016.05.007

zbMATH Keywords

probability theoryhigher-order logicreliability block diagrams (RBDs)virtual data centersvirtualization configuration

Mathematics Subject Classification ID

Reliability, testing and fault tolerance of networks and computer systems (68M15) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formalization of fault trees in higher-order logic: a deep embedding approach
• Towards Formal Fault Tree Analysis Using Theorem Proving
• Formalization of RBD-based cause consequence analysis in HOL
• Formal reliability analysis of combinational circuits using theorem proving
• A framework for formal dynamic dependability analysis using HOL theorem proving

Cites work

• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 847313 (Why is no real title available?)
• A Brief Overview of HOL4
• A theory of type polymorphism in programming
• Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
• On the formalization of the Lebesgue integration theory in HOL
• Towards the formal reliability analysis of oil and gas pipelines

Cited in

(11)

• A framework for formal dynamic dependability analysis using HOL theorem proving
• Formalization of functional block diagrams using HOL theorem proving
• Formal reliability analysis of combinational circuits using theorem proving
• Formal dependability modeling and analysis: a survey
• Formalization of RBD-based cause consequence analysis in HOL
• A framework for formal probabilistic risk assessment using \textsf{HOL} theorem proving
• Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation
• Quantitative mission risk assessment of the satellite propulsion subsystem using PRA method
• Formal reasoning about classified Markov chains in HOL
• Towards the formal reliability analysis of oil and gas pipelines
• Formalization of fault trees in higher-order logic: a deep embedding approach

Describes a project that uses

Uses Software

• HOL
• ML

This page was built for publication: Formalization of reliability block diagrams in higher-order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q334147)