基于系统性质的双向持续检测方法的研究

Architecture-centric, model-based engineering has emerged as key set of technologies to engineer highly-reliable systems. While traditional model-based testing focuses on ensuring the software implementation comply with its designed model, this work concerns particularly the situation that the software model should be updated as well as the implementation. We propose the bi-directional continuous verification, supported by techniques drawn from model-based testing, consistency checking and model checking, to link the model checking phase and the software testing phase together as a feedback loop. This research project targets on dealing with their abstraction levels, identifying and formalizing the differences the software artifacts; automatically and continuously augmenting the verifiable system properties from execution traces of actual running system, as well as locating the root cause of the identified inconsistencies. Our early experimental results show that our proposed method system is able to identify the differences and generating system properties accordingly.

以软件架构为中心，模型驱动为基础的软件工程方法被认为是有效提高软件可信性的方法之一，受到越来越多的关注。然而，传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面，单一的仅仅对系统模型进行验证并检测代码之于模型的一致性无法保证系统模型和软件代码的适时有效更新。本项目提出双向持续检测的概念，设计一套以正向代码测试，匹配测试，和反向模型检测为技术支撑的持续检测过程，有效对接模型验证和系统自动化测试。本项目创新在于从抽象系统模型和具体代码之间的对应入手，借助代码测试技术，寻找系统模型和实际运行代码间的不一致，定义其描述方式；自动生成可机械检验的系统性质以完善模型验证的完备性；基于系统性质自动准确定位系统模型中与实际运行软件的不符，支持体系结构和软件模型的适时更新和迭代。初步研究结果表明，双向持续检测方法能自动有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质。

代码和模型的一致性检测是可信软件领域十分重要的，并且具有挑战的学术研究问题。各种模型驱动的解决方案已经是很多研究课题的主流解决方式。怎样保证代码属性和模型的一致性是本课题的研究重点。只有提取的属性能够真实映射和抽象到模型层面，所构建的模型的健壮性和有效性才能够得到保障。..项目进展顺利，在理论和实践研究方面均取得多项成果。围绕（1）基于Event-B代码和模型的双向一致性持续检测；（2）基于智能应用的质量属性提取和对应检测模型构建；（3）基于智能应用的安全属性提取和对应检测模型构建等主要3个研究方向展开了重点研究。在理论方法和实践方法上均取得了很多突破，圆满完成了各项研究计划和任务，成功实现了预期目标。在项目驱动的研究成果方面，项目课题组成员已经成功发表国际顶级期刊和论文共计15篇（期刊论文2篇，会议论文13篇），其中一区论文，CCF A类期刊或论文10篇，CCF B类期刊和论文2篇，CCF B类期刊或论文2篇，其他一篇。在国际顶级学术会议进行学术报告9次；邀请国内外学者交流访问3次。在在校研究生培养方面，培养博士研究生2名，硕士研究生10名。