Model Checking: Theories,Techniques and Applications
Wenhui Zhang · Dianzi xuebao · 2002
As computer hardware and software systems become more and more complex,how to assure the correctness and reliability of such system sbecomes an urgent problem. Among theories proposed as solutions to this problem, model checking has become a very attractive and appealing approach, because of its simplicity and high level of automation. Research on model checking covers the following subjects: modal/temporal logics,model checking algorithms,efficiency of model checking with respect to time and space(especially space complexity) ,and development of model checking tools.These aspects are closely related. Complexities of model checking algorithms vary very much for different modal/temporal logics, and optimizations are often targeted at certain types of logic formulas. Some new achievements and research directions are also discussed.