基于模块化Abstract-Refine算法框架的软件模型检测方法OA北大核心CSCDCSTPCD
Software Model Checking Method Based on ModularAbstract-Refine Algorithm Framework
Abstract-Refine(抽象—精炼)方法是软件模型检测领域中较为有效的设计思想,具有较高的通用性和效率优势,但目前并没有一个框架可以对其精确进行描述及实现有效的模块化使用和替换.本文提出了一种模块化的Abstract-Refine算法框架,分析和解释了Abstract-Refine算法所接受的输入程序的精细结构和特性,并对Abstract-Re-fine算法和相关子算法运用平衡操作符做以模块化解耦,使得子算法的修改和更换不需要依赖对上层的变更.经过实验验证,本方法可有效实现传统算法模块化解耦,同时不对原算法的性能造成冲击.
王舜;杜晔;韩臻
北京交通大学计算机与信息技术学院,北京100044北京交通大学计算机与信息技术学院,北京100044北京交通大学计算机与信息技术学院,北京100044
信息技术与安全科学
软件模型检测模块化方法抽象—精炼(Abstract-Refine)通用算法抽象程序
《电子学报》 2020 (5)
997-1002,6
国家自然科学基金(No.61672092)
评论