摘要

随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目。具体介绍了模型检测的一些理论,同时将它应用于具体的软件程序,运用模型检测方法对软件进行测试。从而证明了模型检测方法与测试结合对于软件可靠性和正确性所起的巨大作用。