计算机系统的发展对软件提出了更高的要求,相应的提升软件质量这一课题的研究也日益受到从业人员的重视,而软件的可靠性、正确性是保证软件具有高质量的关键因素。目前,在实际的软件验证中,普遍采用的方法是对系统进行大规模的测试,通过输入多个测试用例并检查执行结果是否正确来发现系统中可能存在的问题,但是这种方法通常无法穷举系统所有可能的行为。近些年来,模型验证在验证硬件系统组件和通信协议上的应用已经相当成熟,把模型检测应用于软件系统的验证已经成为备受关注的焦点,且已取得显著成就。许多研究小组开发出了多种实用的软件模型验证工具,如SLAM、MAGIC、JPF等。模型验证技术成功应用于软件系统中的最大阻碍就是程序建模时的状态爆炸问题,本文结合NASA Ames的自动化软件工程小组开源项目JPF(Java PathFinder),在建模—验证—模型细化框架下研究了Java程序模型验证的程序建模过程中缩减程序状态空间的两种方法:程序切片技术和抽象技术。本文的主要工作包括以下几个部分:1.介绍了在建模—验证—模型细化框架下对软件系统进行模型验证的方法。2.在对处理并发机制的并发流程语言(CFCL)进行了形式化描述的基础上,探讨了对多线程程序切片的正确性进行互模拟验证的方法,有效的保证了多线程切片的正确性。3.提出了正确构造多线程程序切片的方法。模型验证与规范化建模语言的紧密结合,极大的推动了验证自动化的发展。4.针对抽象技术的使用会出现反例路径“不可行”的情况,提出了验证反例路径可行性的两种方法:无选择路径搜索和抽象反例导向模拟。