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

Incremental Verification of Aspectual Feature Module Based on Hierarchical State Machine

作　　者：叶俊[1] 谭庆平[1] 李暾[1] 徐建军[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机学报》2009年第9期1773-1781,共9页Chinese Journal of Computers

基　　金：国家自然科学基金项目(60773025);长江学者和创新团队发展计划资助~~

摘　　要：方面化特征模块(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.

关 键 词：方面化特征模块(AFM) 层次状态机(HSM) 增量式验证 面向特征编程范式(FOP) 面向方面编程范式(AOP) 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]