Abstract: Model checking is an important technology of automatic verification. It verifies the modal/proposition properties of concurrent or real-time systems through explicit state exploration or implicit fixpoint computation. It can ensure the correctness of critical application such as communication protocol and digital circuit. In this paper, the development and state-of-art of model checking are expatiated. Two main tactics separately based on automata theory and symbolic structure for concurrent systems are described and the methods to solve state explosion problem are given. Then the methods of model checking for real-time systems and object-oriented designs are introduced. The corresponding known tools for every method are also presented. Finally, the difficulties faced by model checking and its developing trend are analyzed.