A formal verification method: model checking
Yan Xiao-lang · Journal of Zhejiang University(Science Edition) · 2006
Being a formal verification method,model checking is used frequently in hardware and software design.Firstey the Kripke structure which is used to describe the behavior of a system and the CTL logic which is used to describe the property of a system were introduced.Then two model checking algorithms were introduced: one is the labeling algorithm,the other is the algorithm based on fixpoint.In the end,the symbolic model checking which can reduce the possibility of memory explosion was introduced.