Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic