摘要
随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目。具体介绍了模型检测的一些理论,同时将它应用于具体的软件程序,运用模型检测方法对软件进行测试。从而证明了模型检测方法与测试结合对于软件可靠性和正确性所起的巨大作用。
As the computer hardware and software systems become more and mere complex, how to assure the correctness and reliability of such systems becomes an urgent prohlem. 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. In this paper, some theory of model checking is introduced and a software program is tested by model checking method. Hence, the combination of the model checking and software testing is important to the correctness and reliability of software.
出处
《计算机与数字工程》
2006年第2期93-96,共4页
Computer & Digital Engineering
关键词
模型检测
软件测试
强制性逻辑关系
状态爆炸
model checking, software testing, constraint logic relation, status explosion