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

• 作者: 应时 文静 肖芳雄 蒋曹清 高荣
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 抽象解释 终止性验证 模型检测 数据约减
• 年，卷（期）: 2015,（12）
• 所属期刊栏目: 第十三届全国软件与应用学术会议
• 页码范围: 175-180
• 页数: 6页
• 分类号: TP311
• 字数: 9260字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2015.12.038

摘要

面向服务软件中服务间消息的变量值可能存在无穷域的情况,从而导致模型检测时产生状态空间爆炸问题.为了使终止性验证在实践上可行,需要约减模型状态空间的大小,使得计算时间和空间需求合理.为此,基于抽象解释的区间抽象理论扩展了经典区间抽象域方法,并在统一的区间抽象域方法上借助异常控制流图对变量进行区间分析,在此基础上逆向分析得到服务间消息的变量区间集.变量区间上任意值相对于终止性验证是等价性,因此从每一个变量区间集中选取一个代表值,可组成服务间消息变量的约减值,从而为异常处理的终止性验证提供了约减的初始配置,有效避免了状态空间爆炸.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	应时	武汉大学软件工程国家重点实验室	100	849	10.0	26.0
2	文静	武汉大学软件工程国家重点实验室	22	159	7.0	12.0
3	肖芳雄	广西财经学院计算机与信息管理系	19	99	5.0	9.0
4	蒋曹清	广西财经学院计算机与信息管理系	11	25	4.0	4.0
5	高荣	广西财经学院计算机与信息管理系	28	43	4.0	5.0