###
Journal of Software:2016.27(7):1757-1771

ProMiner:系统性质驱动的双向一致性检验框架
葛徐骏,王玲,徐立华,郭建,朱惠彪
(华东师范大学 计算机科学技术系, 上海 200241;上海市高可信计算重点实验室(华东师范大学), 上海 200062)
ProMiner: Bi-Directional Consistency Checking Framework Based on System Properties
GE Xu-Jun,WANG Ling,XU Li-Hua,GUO Jian,ZHU Hui-Biao
(Department of Computer Science and Technology, East China Normal University, Shanghai 200241, China;Shanghai Key Laboratory of Trustworthy Computing(East China Normal University), Shanghai 200062, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 1736   Download 1251
Received:August 14, 2014    Revised:January 27, 2015
> 中文摘要: 在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断扩大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,以更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,对传统基于模型的测试方法的一致性检验进行了扩展,实现了一致性检验框架ProMiner,通过抽取表达模型与代码的不一致的系统性质来自动定位模型中与实际运行系统不匹配的部分,并将其表示为可直接用于模型检测的线性时序逻辑(LTL)表达式,以支持软件模型和代码间双向的一致性检验.实验结果表明,ProMiner可有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性,而且大大减少了人力开销.
Abstract:Model-Driven development is currently a highly regarded software development paradigm among software developers and researchers, and model-based testing techniques are usually applied during the development to ensure the quality of software systems. With the growing size and complexity of software systems, maintaining the consistency between software models and their implementation become more and more challenging. While traditional model-based testing focuses on ensuring the software implementation comply with its designed model, this work addresses particularly the situation where the implementation is modified while software models are left outdated due to workarounds or other unexpected changes during development. The paper presents an automated consistency checking framework, ProMiner, which extends traditional model-based testing with mining software properties that represent the identified inconsistencies as linear temporal logic (LTL). Experiments show that this extended consistency checking technique effectively helps software designer to narrow down the specific locations of software models that need to be updated with respects to its running implementation.
文章编号:     中图分类号:    文献标志码:
基金项目:上海市自然科学基金(13ZR1413000);核高基重大专项(2014ZX01038-101-001);国家自然科学基金(61502170,91118008);国家基金委国际合作项目(中丹)(61361136002);国家基金委创新研究群体项目(61321064) 上海市自然科学基金(13ZR1413000);核高基重大专项(2014ZX01038-101-001);国家自然科学基金(61502170,91118008);国家基金委国际合作项目(中丹)(61361136002);国家基金委创新研究群体项目(61321064)
Foundation items:Natural Science Foundation of Shanghai (13ZR1413000); National Science and Technology Major Project (2014ZX01038-101-001); National Natural Science Foundation of China (61502170, 91118008); NSFC Projects of International Cooperation and Exchanges (61361136002); Science Fund for Creative Research Groups of the National Natural ScienceFoundation of China (61321064)
Reference text:

葛徐骏,王玲,徐立华,郭建,朱惠彪.ProMiner:系统性质驱动的双向一致性检验框架.软件学报,2016,27(7):1757-1771

GE Xu-Jun,WANG Ling,XU Li-Hua,GUO Jian,ZHU Hui-Biao.ProMiner: Bi-Directional Consistency Checking Framework Based on System Properties.Journal of Software,2016,27(7):1757-1771