● 摘要
随着科学技术的快速发展，计算机技术已经融入进了我们生活的各个方面。随着硬件和软件规模和复杂度的增大，导致使用传统测试技术的成本越来越高，并且有一些错误是使用传统测试技术不能够进行验证的。模型检测作为一种形式化自动验证技术可以有效的弥补传统测试技术中的这些问题。
模型检测是和传统的测试技术最大的区别是检测时机的差别，模型检测使用形式化的方法在系统实现前进行测试验证，而传统的测试技术使用用例的方式对系统在实现后进行测试验证。根据Myers的测试理论，模型检测技术这种提前发现问题的方式对成本非常有利。经过近三十年的研究，模型检测已经可以有效的验证很多工作、生活中的问题，如软件、协议等等。模型检测同时也是一门自动化的验证技术，使用不同种类的模型检测器，可以自动的验证许多特定的问题。
模型检测的最大优势就是它的自动化特性，使得手工计算难以解决的问题可以由计算机解决。因此本文初步设计和实现了基于广义可能性测度的模型检测器GPoCheck。其工作过程是这样的：首先对被验证系统和所需验证性质进行建模；然后将模型输入进模型检测器；最后模型检测器实现验证的过程。
本文的主要工作如下：
1. 广义可能性计算树逻辑的模型检测问题已有初步研究，但其不动点语义尚未有系统研究。本文给出广义可能性计算树逻辑的不动点语义解释。利用不动点语义可以完善广义可能性模型检测算法，为实现模型检测器打好基础。
2. 根据现阶段广义可能性计算树逻辑模型检测理论，初步实现了一个基于广义可能性测度的模型检测器GPoCheck，使用户可以自动化验证系统性质。