软件产品线工程通过管理软件产品的可变性和共性特征,提高软件开发效率,节约开发成本。模型检测是一种自动形式化验证技术。随着软件产品线在安全关键领域的广泛应用,对软件产品线的模型检测已成为软件验证领域的一个重要研究方向。在软件产品线开发的早期阶段,由于特征的复杂性,系统设计中往往存在不确定信息。然而,现有的软件产品线模型检测对这种情况下的建模和验证支持不足。为此,本文提出一种基于多值逻辑对软件产品线的不完备设计进行建模和验证的方法,可以描述软件产品线设计初期存在的不确定信息,将模型检测提前到系统开发的早期阶段进行,及时发现错误,降低后期的修复成本。本文的具体工作包括以下几个方面。首先,本文以世界双格作为理论基础,提出一种多值模型——基于双格的特征迁移系统,实现对包含不确定信息的软件产品线进行建模,并通过投影和精化关系定义特定软件产品的不完备模型和具体模型。然后,采用动作计算树逻辑描述系统的时序属性,定义动作计算树逻辑在基于双格的特征迁移系统上的语义,提出基于双格的多值模型检测。进一步,为实现基于双格的多值模型检测,一方面,提出从基于双格的特征迁移系统到多值Kripke结构的等价转换方法,开发了辅助工具BPMCA,使得能够结合现有的多值模型检测工具?Chek实现软件产品线的多值模型检测;另一方面,提出针对单个特征的分解方法,将多值模型检测问题分解为多个三值模型检测问题,降低模型检测的复杂度。最后,对文献中的软件产品线实例进行实验分析,验证了方法的有效性。