ProMiner:系统性质驱动的双向一致性检验框架

来源：软件学报杂志2016年第7期北京时间：

作者：葛徐骏,王玲,徐立华,郭建,朱惠彪

单位：葛徐骏，华东师范大学 计算机科学技术系, 上海 20024111,王玲，华东师范大学 计算机科学技术系, 上海 20024102,徐立华，华东师范大学 计算机科学技术系, 上海 20024103,郭建，上海市高可信计算重点实验室(华东师范大学), 上海 20006204,朱惠彪，上海市高可信计算重点实验室(华东师范大学), 上海 20006205

摘要：在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断扩大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,以更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,对传统基于模型的测试方法的一致性检验进行了扩展,实现了一致性检验框架ProMiner,通过抽取表达模型与代码的不一致的系统性质来自动定位模型中与实际运行系统不匹配的部分,并将其表示为可直接用于模型检测的线性时序逻辑(LTL)表达式,以支持软件模型和代码间双向的一致性检验.实验结果表明,ProMiner可有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性,而且大大减少了人力开销.

关键词：一致性检验;模型检测;基于模型的测试;线性时序逻辑

基金资助：上海市自然科学基金(13ZR1413000);核高基重大专项(2014ZX01038-101-001);国家自然科学基金(61502170,91118008);国家基金委国际合作项目(中丹)(61361136002);国家基金委创新研究群体项目(61321064)