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

作者简介:

通讯作者:

中图分类号:

基金项目:

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


ProMiner: Bi-Directional Consistency Checking Framework Based on System Properties
Author:
Affiliation:

Fund Project:

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)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断扩大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,以更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,对传统基于模型的测试方法的一致性检验进行了扩展,实现了一致性检验框架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.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2014-08-14
  • 最后修改日期:2015-01-27
  • 录用日期:
  • 在线发布日期: 2016-07-07
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号