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

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

一种可重用的方面化特征模块的构建方法

针对互联网环境下存在丰富多样的软件资源,为了能够有效地重用已有的软件资源,需要对软件资源进行模块化,基于面向方面的编程思想的方面化特征模块为软件模块化,构建提供了1种新型的软件构建方法,该方法能够根据不同方面抽象出软件特征形成的具有相应特征的软件模型,封装成为可重用的AFM模块,利用逻辑程序语言描述方面接口,实现业务逻辑层面的软件重用,提高了软件重用的层次与范围.

用方面化特征模块开发OpenRISC1200软核

对OpenCores上的OpenRISC1200项目(简称OR1200)的统计发现,条件编译指令的使用高达714次,嵌入在条件编译指令间的代码占代码总量的61.60%。条件编译在硬件开发中被大量使用,但在软件开发时却并不提倡。因此,本文提出用方面化特征模块(AFM)开发硬件系统,以避免条件编译指令的使用。作为案例,本文给出用AFM重新开发OR1200项目的过程,它使得OR1200各features的开发从同时开发变为顺序开发,使得服务于各feature的代码从纠缠在一起变为相互独立,有利于OR1200的维护和调试。最后,基于OR1200的开发过程,本文建立了一套AFM开发方法下的硬件系统的形式化模型,它是进一步的形式化验证工作的基础。