基于抽象解释的服务间消息的数据约减  

Data Reduction Analysis for Message between Services Based on Abstract Interpretation

作　　者：蒋曹清[1] 肖芳雄[1] 高荣[1] 应时[2] 文静[2] 

机构地区：[1]广西财经学院计算机与信息管理系,南宁530003 [2]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机科学》2015年第12期175-180,共6页Computer Science

基　　金：国家自然科学基础重点项目(91118003;61272113;61272108);国家自然科学基金项目(61070012;61170022;6126200);广西高校科学技术研究项目(YB2014349)资助

摘　　要：面向服务软件中服务间消息的变量值可能存在无穷域的情况,从而导致模型检测时产生状态空间爆炸问题。为了使终止性验证在实践上可行,需要约减模型状态空间的大小,使得计算时间和空间需求合理。为此,基于抽象解释的区间抽象理论扩展了经典区间抽象域方法,并在统一的区间抽象域方法上借助异常控制流图对变量进行区间分析,在此基础上逆向分析得到服务间消息的变量区间集。变量区间上任意值相对于终止性验证是等价性,因此从每一个变量区间集中选取一个代表值,可组成服务间消息变量的约减值,从而为异常处理的终止性验证提供了约减的初始配置,有效避免了状态空间爆炸。Infinite values of variable range of message between services may exist in service-oriented software,which results in the state space explosion situation when checking model. In order to make termination rerification feasible in practice, the size of the state space must be reduced which makes computing time and space demand reasonable. In this paper,based on interval abstract theory of abstract interpretation, we extended the classic interval abstract domain methods, carried out variable interval analysis on exception control flow graph with abstract domain methods of the unification interval. On this basis, interval set of message variables between services is obtained by the reverse analysis. An arbitrary value on a variable interval is equivalence relative to the termination of the verification, so reduction values of message variables between services can be gotten through selecting a representative value from every variable interval sets,which provides the reduced initial configuration for termination verification of exception handling, effectively avoides the state space explosion.

关 键 词：抽象解释 终止性验证 模型检测 数据约减 

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