Abstract: We proposed a realtime method to diagnose dynamic systems with model checking. This method utilizes the efficiency of verification of model checking on a large state space to diagnose. It enhances real time diagnosis in AI region. We built a platform based model checking to integrate modeling, testing diagnosability and performing diagnosis, the result proves that our method is feasible.

Key words: modelbased diagnosis, diagnosability, bounded model checking, symbolic model checking