In model-based fault injection, user-specified faults may be (automatically) injected into the nominal model (i.e., without faults) of the system of interest (see Figure 3.2). In this approach, the user can specify the faults to be injected manually, or by picking them from a predefined library. For instance, the xSAP tool [MBI1] provides libraries to specify the most common failure patterns (e.g., stuck-at faults, non-deterministic faults, ramp-down, etc.), to specify their dynamics (e.g., permanent faults, sporadic faults, etc.) and to instantiate them using specific parameters. The resulting model after fault injection is called extended model and can be analysed using safety assessment techniques to produce artefacts such as FTs and FMEA tables. In xSAP, both the nominal and the extended model are written in the SMV language, and the extended model is generated automatically using the given fault specifications. Similar techniques can be used to analyse the effectiveness of fault detection, isolation, and recovery procedures. Faults to be injected may include different classes of faults (HW/SW/functional) at different levels of abstraction.