Probabilistic Model-Checking Support for FMEA

Failure Mode and Effect Analysis (FMEA) is a method for assessing cause-consequence relations between component faults and hazards that may occur during the lifetime of a system. The analysis is typically time intensive and informal, and for this reason FMEA has been extended with traditional model checking support. Such support does not take into account the probabilities associated with a component fault occurring, yet such information is crucial to developing hazard reduction strategies for a system. In this paper we propose a method for FMEA which makes use of probabilistic fault injection and probabilistic model checking. Based on this approach safety engineers are able to formally identify if a failure mode occurs with a probability higher than its tolerable hazard rate.