Experience with fault injection experiments for FMEA

Failure Modes and Effects Analysis (FMEA) is a widely used system and software safety analysis technique that systematically identifies failure modes of system components and explores whether these failure modes might lead to potential hazards. In practice, FMEA is typically a labor-intensive team-based exercise, with little tool support. This article presents our experience with automating parts of the FMEA process, using a model checker to automate the search for system-level consequences of component failures. The idea is to inject runtime faults into a model based on the system specification and check if the resulting model violates safety requirements, specified as temporal logical formulas. This enables the safety engineer to identify if a component failure, or combination of multiple failures, can lead to a specified hazard condition. If so, the model checker produces an example of the events leading up to the hazard occurrence which the analyst can use to identify the relevant failure propagation pathways and co-effectors. The process is applied on three medium-sized case studies modeled with Behavior Trees. Performance metrics for SAL model checking are presented.