电子学报 ›› 2020, Vol. 48 ›› Issue (5): 997-1002.DOI: 10.3969/j.issn.0372-2112.2020.05.022

• 学术论文 • 上一篇    下一篇

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

王舜, 杜晔, 韩臻   

  1. 北京交通大学计算机与信息技术学院, 北京 100044
  • 收稿日期:2019-03-29 修回日期:2019-09-02 出版日期:2020-05-25 发布日期:2020-05-25
  • 作者简介:王舜 男,1988年生,河南洛阳人,北京交通大学博士生,主要研究方向为形式化方法、程序分析技术、信息安全等.E-mail:shunwang@bjtu.edu.cn;杜晔 男,1978年生,黑龙江哈尔滨人,北京交通大学教授、博士生导师,主要研究方向为网络安全、态势感知、软件可靠性分析与评估等.E-mail:ydu@bjtu.edu.cn;韩臻 男,1962年生,浙江宁波人,北京交通大学教授、博士生导师,主要研究方向为可信计算、系统安全、保密技术等.E-mail:zhan@bjtu.edu.cn
  • 基金资助:
    国家自然科学基金(No.61672092)

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

WANG Shun, DU Ye, HAN Zhen   

  1. School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China
  • Received:2019-03-29 Revised:2019-09-02 Online:2020-05-25 Published:2020-05-25

摘要: Abstract-Refine(抽象—精炼)方法是软件模型检测领域中较为有效的设计思想,具有较高的通用性和效率优势,但目前并没有一个框架可以对其精确进行描述及实现有效的模块化使用和替换.本文提出了一种模块化的Abstract-Refine算法框架,分析和解释了Abstract-Refine算法所接受的输入程序的精细结构和特性,并对Abstract-Refine算法和相关子算法运用平衡操作符做以模块化解耦,使得子算法的修改和更换不需要依赖对上层的变更.经过实验验证,本方法可有效实现传统算法模块化解耦,同时不对原算法的性能造成冲击.

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

Abstract: 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.

Key words: software model checking, modularity, Abstract-Refine, general algorithm, abstract program

中图分类号: