Importance measures provide a systematic approach to scrutinize the critical system components, which are extremely beneficial in making important decisions, such as prioritizing reliability improvement activities, identifying weak-links and effective use of given resources. Using these importance measures, a typical approach is to obtain a criticality value for each system component and then rank the components in an ascending manner. Simulations tools generally require expensive computations to perform importance measure analysis, which may not be doable for large systems. A more practical approach is to utilize these importance measures to obtain all the necessary conditions by proving a relationship describing the relative importance between any pair of components in a system. In this paper, we propose to use higher-order-logic (HOL) theorem proving to verify such relationships and thus making sure that all the essential conditions are accompanied with the proven property. In particular, we formalize the commonly used importance measures, such as Birnbaum and Fussell-Vesely, and conduct a formal importance measure analysis of a railway signaling system at a Moroccan level crossing for illustration purpose.