关键词: 时态逻辑,模型检验,抽象解释,抽象模型检验

Abstract: Model checking is an important technique in software/hardware verification,and it has become an enormous system of methodologies．Now we investigated the contents of model checking from three categories which are standard methods,abstract interpretation methods and integrate methods respectively．The aim of this survey is making one to have a complete impression about model checking．In this way one may fully understand and grasp the spirits and concrete contents of every method in model checking．The studies help in applying these methods to the piratical software/hardware verification,and furthermore,inspired of this,one may develop new model checking theories or new methods or tools of model checking.

Key words: Temporal logic,Model checking,Abstract interpretation,Abstract model checking