随着互联网的飞速发展和软件开发的多样化,软件复杂性和需求量急剧增长。然而,伴随产生的软件质量与安全问题也日渐突出。近些年来,由于软件错误导致的严重事故屡见不鲜,例如,1994年英特尔的奔腾微处理器芯片的浮点计算单元出现的一个Bug使得其损失4.75亿美元。因此,软件的可靠性与安全性显得尤为重要,并受到了更为广泛的关注。传统的确保软件质量和安全的方法主要是通过软件测试完成的,系统行为的正确性、可靠性和安全性必须依靠长时间不间断的测试,逐渐发现存在的各种问题并及时进行更正。但是,测试也仅仅是为了证明软件存在错误而不能保证没有错误,由此看来这种方式缺乏根本保障。而建立在严格数学基础上的形式化方法无疑是一种精密且可靠的软件技术,特别适合于软、硬件系统的描述、开发和验证,因而越来越受到数学、计算机、人工智能等领域研究者的青睐。建模、仿真和验证语言(Modeling,Simulation and Verification Language,MSVL)是一个时序性逻辑程序设计语言,具有丰富的类型系统,能很好地对并行和实时系统进行形式化规范和验证。而目前关于MSVL程序的验证工具大多数基于模型检测技术。Coq是一个由法国国家信息与自动化研究所(INRIA)开发的定理证明辅助工具,不仅可以用来开发满足规范说明的程序,还可以用来开发证明并能从证明中生成可靠的程序和模块。本文主要研究的是一种基于定理证明器Coq的MSVL程序验证方法,具体研究成果如下:(1)针对关于MSVL程序的定理证明还没有很好地被工具支持的问题,本文提出了一种基于公理语义的MSVL程序定理证明方法并开发了一个基于Coq的MSVL程序定理证明器。首先使用Coq规范语言Gallina描述MSVL变量、表达式和函数;然后使用Gallina描述MSVL语句和衍生语句;最后在Coq中形式化MSVL公理系统的公理和推导规则。基于以上的定义,Coq可以很好地识别MSVL程序。(2)根据提出的验证方法,对于具体实例的验证,首先使用MSVL对问题建模,然后抽取出相关待证性质,最后使用Coq策略对定理进行半自动化证明。证明过程交互式进行并采用反向推理,如果用户所选策略的前向条件可满足,则策略的应用使得当前目标被化简为一个或多个待证的子目标,琐碎的细节被自动地证明,反之则策略有误。当所有目标解决后,证明结束,性质验证完成。