软件复用是解决软件危机的有效途径。实现软件复用的一种可行办法是在特定的应用领域内组织实施可复用资产的生产活动，即领域工程。特征建模是领域工程中捕获可复用需求的一种重要技术手段。它将软件需求组织为特征,并以特征为基本单位建立需求层的复用模型。在开发新的应用软件时，可以方便地通过对领域特征模型的定制（对一组可选择的特征进行绑定或删除的操作），实现有效的、大粒度的复用。　　 特征模型定制中的一个重要问题是验证问题。对特征模型的验证有两个目的：第一，在定制活动前，检查出特征模型的约束之间可能存在的冲突；第二，在对特征模型定制之后，检查出定制决策导致的冲突。　　 在已有的关于模型检查的研究中，形式化验证技术一般包含三个方面：待验证模型的形式化表述、待验证性质的形式化表述和验证模型是否满足性质的方法。在特征模型形式化验证的研究中，前两方面的问题在很大程度上已经被解决，但特征模型形式化验证方法的研究尚存在不足。研究者一般认为，既然可以一组用命题逻辑表达式表示特征模型的约束，那么可以直接使用第三方逻辑引擎（如SAT-solver，SMV）验证这组命题逻辑表达式是否满足验证准则。然而，第三方逻辑引擎一般是为通用的问题设计的，并不会为特征模型做任何优化。实践表明，在特征模型规模不太大时，这些方法就会发生指数爆炸。　　 本文提出了一种对特征模型的组合验证方法。其基本思想是将特征模型验证问题分解为较小的子问题，然后以组合的方式对这些小问题进行验证。本文论证，特征模型验证问题的复杂度不是与特征数量成指数关系，而是与一个称作最大独立非平凡特征子集的集合的基数成指数关系。我们用c代表这个集合的基数，用n代表特征的数量，那么本文的方法将特征模型验证问题的复杂度从0(2n)改进为0(n)+0(2c)。直观上，在实际可能构造出的大规模的特征模型中，c必然远小于n。　　 本文的主要工作包括：(1)提出对特征模型的一种组合验证方法，并给出其正确性的证明：(2)基于第三方逻辑引擎BDD，使用该方法实现特征模型的验证器；(3)设计了测试用例生成算法，对方法的效率进行了评估。