摘要
Abstract-Refine(抽象—精炼)方法是软件模型检测领域中较为有效的设计思想,具有较高的通用性和效率优势,但目前并没有一个框架可以对其精确进行描述及实现有效的模块化使用和替换.本文提出了一种模块化的Abstract-Refine算法框架,分析和解释了Abstract-Refine算法所接受的输入程序的精细结构和特性,并对Abstract-Refine算法和相关子算法运用平衡操作符做以模块化解耦,使得子算法的修改和更换不需要依赖对上层的变更.经过实验验证,本方法可有效实现传统算法模块化解耦,同时不对原算法的性能造成冲击.
Abstract-Refine is a relatively effective method in the field of software model checking,which has the advantages of high generality and efficiency.However,there is no framework for precise description and effective modular use or replacement of this method so far.This paper introduces a modular Abstract-Refine algorithm framework which analyzes and explains the structure of input program in fine-grained level.Also,this method modularly decouples Abstract-Refine algorithm from its sub-algorithms with the balancing operator,so that any modifications on sub-algorithms will not affect the upper level.Experiments verify that our approach can effectively implement modular decoupling of traditional algorithms,and will not impact the performance of original algorithms.
作者
王舜
杜晔
韩臻
WANG Shun;DU Ye;HAN Zhen(School of Computer and Information Technology,Beijing Jiaotong University,Beijing 100044,China)
出处
《电子学报》
EI
CAS
CSCD
北大核心
2020年第5期997-1002,共6页
Acta Electronica Sinica
基金
国家自然科学基金(No.61672092)。
