现代计算机技术已经时时刻刻伴随着我们的生活,随着现代计算机软件和硬件的设计越来越复杂,对软件和硬件的测试也变得越来越复杂,不仅需要消耗大量的人力物力成本,而且使用传统的检测技术也有一定的局限性,对于生活中真实存在的一些不确定性因素,存在着一定的检测缺陷,从而导致检测失败。1981年,Clarke和Emerson以及Quielle和Sifakis提出了模型检测的理论,作为一种形式化的自动验证技术,为我们解决这些检测问题提供了一个很好的解决方案。对比传统的检测技术,模型检测技术有着一系列的优势,比如可以在系统实现之前对系统进行验证,提前发现问题,节约检测成本等等,这些检测一般会使用基于模型检测理论实现的模型检测器去进行验证,传统的模型检测器大多是基于一些经典的理论而实现的,随着我们研究的深入,我们发现现实生活中有着大量的不确定信息,这样使用传统理论实现的模型检测器无法解决这些问题。而多值模型检测理论的出现,利用在格上构建不确定信息,结合多值计算树逻辑,通过构建的多值可能性Kripke结构模型,有效的解决了这些问题。同时为了实现模型检测技术的自动化验证的特性的优势,本文基于多值可能性的多值计算树逻辑的模型检测理论,设计了多值Kripke结构在计算机中的存储结构,计算模块等等,实现了一个多值模型检测器MvChecker,使得用户可以自动化的验证系统性质。本文的具体工作如下:(1)对理论中定义的多值模型Kripke结构,从计算机存储的方面进行了数据结构上的设计,并且分析了时间复杂度,尽量用最优的数据结构对状态和转移函数进行存储,使得模型检测器能够读入更多的数据量,计算出更多的状态,并且有效缓解在一定数据量下的状态爆炸的问题。(2)根据模型检测理论的流程图,分析出模型检测器的结构,设计了模型检测器的框架,从用户输入的模型以及性质,到如何转换模型和性质到计算机中,如何对转换之后的数据进行计算,以及怎么验证用户的性质,完成检测后检测结果的输出,并对时间复杂度进行了分析,对设计的模型检测器的测试,完成了模型检测器设计的一整套流程。