基于模块化Abstract-Refine算法框架的软件模型检测方法  

Software Model Checking Method Based on Modular Abstract-Refine Algorithm Framework

作　　者：王舜 杜晔[1] 韩臻[1] WANG Shun;DU Ye;HAN Zhen(School of Computer and Information Technology,Beijing Jiaotong University,Beijing 100044,China)

机构地区：[1]北京交通大学计算机与信息技术学院,北京100044

出　　处：《电子学报》2020年第5期997-1002,共6页Acta Electronica Sinica

基　　金：国家自然科学基金(No.61672092)。

摘　　要：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.

关 键 词：软件模型检测 模块化方法 抽象—精炼(Abstract-Refine) 通用算法 抽象程序 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]