基于层次状态机的方面化特征模块的增量式验证

作者：叶俊; 谭庆平; 李暾; 徐建军

来源：计算机学报, 2009, (09): 1773-1781.

• 方面化特征模块(AFM)
• 层次状态机(HSM)
• 增量式验证
• 面向特征编程范式(FOP)
• 面向方面编程范式(AOP) Aspectual Feature Module(AFM)
• Hierarchical State Machine(HSM)
• incremental verification
• Feature-Oriented Programming(FOP)
• Aspect-Oriented Programming(AOP)

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

• 单位
  中国人民解放军国防科学技术大学