中文摘要：

方面化特征模块（AFM）是最新提出的软件产品线（SPL）编程范式，能解决现有SPL编程范式存在的问题，但由于AFM范式同时存在模块的并发组合和顺序组合，现有的组合验证技术和模块化模型检验技术并不适用于AFM程序的验证，且目前还未见到针对AFM的验证方法，这制约了AFM范式的应用．文中首次为AFM范式建立了形式化模型，并基于此模型提出一种AFM程序的增量式的验证方法．该方法可以从一个小规模的AFM程序的验证开始，以后每次只添加对新组合的AFM模块的验证，因此可避免直接验证大型AFM程序时可能由于模型的规模太大而无法验证的问题．

英文摘要：

Aspectual Feature Module （AFM） is a newly-proposed Software Product Line （SPL） programming paradigm, which solves the problems of existing SPL paradigms. But its inherent hybrid of parallel composition and sequential composition of modules prohibits the application of conventional verification technology, e.g. compositional verification and modular model chec- king. There is no verification method for AFM paradigm now, which restricts its application. This paper firstly establishes a formal model for AFM paradigm, and proposes an incremental verification method based on this model. This method starts from the verification of a small-scale AFM program and increases with the verification of just the recently-composed AFM module. It can avoid the state space exploration problem caused by a direct verification of a large-scale AFM program.