基于模型检测的软件动态演化一致性保障机制研究

The consistency assurance mechanism during evolution is an active research topic of software evolution in open environment. Traditional model checking techniques focus on the internal states' representation and manipulation in a general sense. Due to the state explosion problem, it is difficult to verify the consistency properties of large-scale systems. To address this problem, the proposal consists of the following parts: 1. To investigate the underlying patterns and behavior characteristics of software evolution in open environment,and distill a novel domain modeling mechanism, i.e., an architecture centric domain model; 2. Based on the characteristics of the domain model, to design the state generation algorithms accordingly so as to reduce the number of states which are essentially the same but regarded as different ones by general model checkers; 3. To investigate the structure characteristics of consistency specifications, translate the global properties into a set of semantics-equal local properties, and leverage the compositional reasoning techniques to verify those local properties separately in parallel. The research aims to enhance the scales of verified systems and improve the efficiency of verification compared to the current practice in the field, and provide as an assurance mechanism to conduct dynamic evolution correctly and effectively.

演化一致性保障技术是开放环境下软件演化研究的热点问题。传统的模型检测方法着力于通用的模型内部状态的表达和处理方式，由于状态空间爆炸问题，难以直接利用该技术来验证较大规模软件一致性。本课题拟针对此问题展开研究，主要包括：1，研究开放环境下软件演化的形态、行为特征，提炼一种新的以体系结构为中心的领域建模机制2，根据领域模型特征，针对性地设计内部状态生成算法，避免那些本质相同但在通用模型检测工具中认为是不同的状态产生；3，研究一致性规约属性的结构特征，将全局属性转换为一系列等价局部属性，利用组合推理技术，并行化分别验证。通过以上研究，在待验证系统的规模和验证效率等方面取得进展与突破，为软件动态演化正确有效地实施提供技术保障。

动态演化能力是开放环境下软件形态的一种重要特征，动态演化的关键问题之一就是演化的一致性问题，获得了广泛的关注，有大量的工作从不同角度对此问题进行研究。本项目主要研究了如何引入模型检测技术，保障软件演化模型与规约的一致性，并针对验证过程的状态空间爆炸问题，采用多种方式，如对称化简技术、组合推理技术等来进一步提高待验证系统的规模和效率。本项目取得主要成果如下：针对开放环境下软件系统的层次式结构特征，提出用层次式时间自动机建模，给出严格的操作语义模型，该项成果发表在计算机科学技术学报(JCST)上；提出了一个层次平展化算法，并用互模拟理论证明该算法的正确性，将层次式时间自动机模型等价转化为平展化时间自动机模型，从而可以用现有模型检测工具如UPPAAL等对之进行形式化的验证，该项相关工作发表在软件学报，中国科学（信息科学），国际软件过程会议(ICSSP)等，平展化算法获得了国家发明专利；在属性规约验证方面，针对图文法建模方式不能针对反应式规约的相关属性进行描述验证，提出了一种轻量级的针对反应式规约的相关属性验证的方法，并且根据应用领域特征，采用对称化简、组合验证等技术进一步压缩状态空间，缓解了状态爆炸问题，相关工作发表在计算机前沿(FCS)上；开发的基于ECLIPSE富客户端(rich client)的原型系统，一个支持开放系统动态演化的中间件平台，相关论文发表在Computing期刊上；此外，本项目还做了一些拓展性研究，例如针对开放环境中的不确定性建模问题，开放系统中的协议验证问题，软件的缺陷前馈预测问题等，相关工作发表在ICWS, ICSME, ICA3PP, 中国科学(信息科学)等会议或期刊上。本项目系统地针对了软件动态演化过程中的一致性验证等问题展开研究，在待验证系统的规模和效率上取得了一定的进展和突破，取得了较为丰硕的成果，较好地完成了项目计划目标。