In this paper, we present a rigorous design of a Fault Diagnosis and Isolation algorithm. The system is modelled as a hybrid system with a network of parallel components. The requirement is specified in Duration Calculus, a dense time temporal logic. We use traditional program logic, suitably extended, to verify the discrete component and subsequently derive a number of properties of the system. Finally, the requirement is shown to be satisfied by proving that it can be deduced from the system properties.