近年来,空指针引用故障引发的软件安全问题层出不穷,给软件开发公司及用户带来了极大的困扰,也引起了国内外对之进行故障发现的研究热潮。数组空指针故障是空指针引用故障的一种,也是程序中存在的比较常见的问题,由于它在程序中比较隐蔽,用动态测试方法耗时又耗力且很难达到全面覆盖的效果。本文提出一种基于模型检测及抽象解释理论的数组空指针故障静态测试方法。首先将数组空指针故障进行定义和分类,把它总体分为函数内和函数间的数组空指针故障,然后将数组空指针引用问题抽象为一类故障模型,并以故障模式状态机来形式化描述此类故障模型,为了支持数组空指针故障发现对数组类经典区间域进行了扩展,并通过函数摘要的生成传递与使用支持数组空指针故障的全局分析与检测,最后根据故障状态机的创建条件及待检测代码的语义信息确定是否创建该类型的状态机,并将创建的状态机实例置于控制流图入口节点,根据数据流分析的结果对故障状态进行迭代以检测数组空指针故障。本文提出的方法已在DTSJava (Defects Testing System for Java, Java缺陷检测系统)中应用实现。文章实验部分通过使用未实现本文方法的DTSJava5.0版本与实现了本文方法的DTSJava6.0版的对比以及使用DTSJava6.0与Findbugs, Klockwork K8的实验数据对比,阐明本法的实用和有效性。