基于双格的软件产品线模型检测

Model Checking of Software Product Line Based on Bilattices

软件产品线在保留每个产品的可变性前提下通过最大化产品间的共性实现资源的再利用,从而提高生产效率和节约生产成本。近年来,基于特征的状态迁移系统应用于软件产品线的建模和验证中。然而现有的方法不能很好地支持软件产品线中存在的信息不确定和不一致的情况。为此,首先提出一种基于双格的特征迁移系统,用于软件产品线的行为建模,采用投影的方法定义产品的行为模型;然后采用动作计算树逻辑描述系统的时序属性,并且给出它在新系统上的语义,用于支持基于双格的模型检测;最后,采用多值模型检测工具χchek对方法的有效性进行实验分析。

Software product line（SPL）maximizes the commonality between similar software products to reduce production costs and improve productivity.Recently,state transition systems based on features have been widely used in behavioral modeling and verification of SPLs.However,they can＇t nicely support uncertain and inconsistent information.Therefore,firstly a formalism,bilattice-based featured transition systems（BFTS）,was proposed for model checking of SPLs with uncertain and inconsistent information,where product was defined via projection.Furthermore,action computation tree logic（ACTL）was used to describe temporal properties;its semantics on BFTS was defined for model checking.Finally,based on multi-valued model checkerχchek,a case study was conducted to illustrate the effectiveness of our approach.