A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving