Dynamic fault trees, qualitative analysis, quantitative analysis, higher-order logic, theorem proving, HOL4