软件运行出现故障之后,软件故障定位非常困难。传统的软件定位方法主要是结合测试技术,使用有针对性的测试,发现软件中存在的特定缺陷,再利用其他辅助技术找出故障原因并定位故障,这些定位方法主要依赖于开发者的经验,存在过程复杂、依赖性强和通用性不高等缺陷,不能满足软件故障自动定位的要求。形式化方法是软件故障自动定位方法研究的基础,形式化方法中模型验证以其高效、自动化的优点使其在越来越多的领域中被运用。模型验证是一种对有限状态迁移系统验证其时态逻辑性质的重要方法,由于模型验证过程完全自动化,所以非常适合于验证复杂系统性质的要求。如果能够将模型验证技术运用在故障定位技术中,则可在一定程度上支持软件故障自动定位研究,从而成为一个提高软件可靠性的重要手段。本文针对软件故障自动定位研究的需要,提出了一种基于模型验证的软件故障定位方法,并在此方法的基础之上给出了一个故障定位原型系统框架并部分实现了自动化。经实验表明,该方法能大大减少在故障定位过程中代码审查的范围,能快速有效地定位软件故障,从而为软件故障定位提供了一种新途径。本文的主要工作包括以下几个部分：1)建立支持软件故障定位的形式模型。研究了软件模型验证的基本过程,完成了从软件源代码到软件形式模型的建立,详细设计了建模过程中涉及的数据结构和算法,并对算法进行了性能分析。2)基于模型验证的故障定位方法研究。在模型建立的基础之上,建立了建模—验证—定位过程的故障定位系统的框架,结合模型验证工具进行语义转换,编写适合模型验证工具的验证程序,构造待验证性质的形式化公式,应用模型验证工具检验模型得到反例路径,结合抽象模型分析反例路径信息,通过抽象模型和具体系统状态之间的对应关系,进行反例解释,逆向映射建模过程,最终实现了故障定位。3)采用模型验证的方法进行故障定位试验。对一个多线程访问共享资源的Java源程序,采用2)中提出的模型验证方法进行故障定位试验,并分析了用该方法进行故障定位的优缺点。