计算机科学 ›› 2015, Vol. 42 ›› Issue (12): 175-180.

• 第十三届全国软件与应用学术会议 • 上一篇    下一篇

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

蒋曹清,肖芳雄,高 荣,应 时,文 静   

  1. 广西财经学院计算机与信息管理系 南宁530003,广西财经学院计算机与信息管理系 南宁530003,广西财经学院计算机与信息管理系 南宁530003,武汉大学软件工程国家重点实验室 武汉430072,武汉大学软件工程国家重点实验室 武汉430072
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受国家自然科学基础重点项目(91118003,61272113,61272108),国家自然科学基金项目(61070012,61170022,6126200),广西高校科学技术研究项目(YB2014349)资助

Data Reduction Analysis for Message between Services Based on Abstract Interpretation

JIANG Caoqing, XIAO Fangxiong, GAO Rong, YING Shi and WEN Jing   

  • Online:2018-11-14 Published:2018-11-14

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

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

Abstract: Interpretation JIANG Cao-qing1 XIAO Fang-xiong1 GAO Rong1 YING Shi2 WEN Jing2 (Department of Computer and Information Management,Guangxi University of Financial and Economics,Nanning 530003,China)1 (State Key Lab of Software Engineering,Wuhan University,Wuhan 430072,China)2 Abstract 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.

Key words: Abstract interpretation,Termination verification,Model check,Data reduction

[1] Cousot P,Cousot R.A gentle introduction to formal verification of computer systems by abstract interpretation[M]∥Esparza J,Grumberg O,Broy M,et al.,eds.Logics and Languages for Reliability and Security,NATO Science Series III:Computer and Systems Sciences.IOS Press,2010:1-29
[2] Weissbach M,Zimmermann W.A service-level agreement ap-proach towards termination analysis of service-oriented systems[C]∥International Conference on Cloud Computing,GRIDs,and Virtualization.Rome,Italy,2011:26-31
[3] Weissbach M,Zimmermann W.Termination analysis of business process workflows[C]∥Proceedings of the 5th International Workshop on Enhanced Web Service Technologies,Ayia Napa(Cyprus,2010).New York:ACM,2011:18-25
[4] 李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术[J].软件学报,2008,19(1):17-26 Li Meng-jun,Li Zhou-jun,Chen Huo-wang.Program Verification Techniques Based on the Abstract Interpretation Theory[J].Journal of Software,2008,9(1):17-26
[5] Dams D.Abstraction in software model checking:principles and practice[C]∥Proceedings of the 9th International SPIN Workshop:Model Checking Software.LNCS 2318,2002:14-21
[6] Cousot P,Cousot R.An abstract interpretation framework for termination[C]∥Conference Record of the 39th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages.ACM Press,2012:245-258
[7] 姬孟洛,王怀民,李梦君,等.一种基于抽象解释和通用单调数据流框架的值范围分析方法[J].计算机研究与发展,2006,43(11):2020-2026 Ji Meng-luo,Wang Huai-min,Li Meng-jun,et al.An Value Range Analysis Based on Abstract Interpretation and Generalized Monotone Data Flow Framework[J].Journal of Computer Research and Development,2006,3(11):2020-2026
[8] Clarke E M,Grumberg O,Long D E.Model checking and ab-straction[J].ACM Transactions on Programming Languages and Systems,1994,16(5):1512-1542
[9] 蒋曹清,应时,文静,等.面向服务软件中异常处理的形式化建模方法[J].西安交通大学学报,2013,47(4):118-124 Jiang Cao-qing,Ying Shi,Wen Jing,et al.A Modeling Approach for Exception Handling in Service-Oriented Software[J].Journal of Xi’an Jiaotong University,2013,7(4):118-124
[10] 蒋曹清,应时,文静,等.面向服务软件异常处理过程的可终止性验证[J].计算机科学与探索,2012,6(3):208-220 Jiang Cao-qing,Ying Shi,Wen Jing,et al.Verification of Termination for Exception Handling Process in Service-Oriented Software[J].Journal of Frontiers of Computer Science & Techno-logy,2012,6(3):208-220

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75, 88 .
[2] 夏庆勋,庄毅. 一种基于局部性原理的远程验证机制[J]. 计算机科学, 2018, 45(4): 148 -151, 162 .
[3] 厉柏伸,李领治,孙涌,朱艳琴. 基于伪梯度提升决策树的内网防御算法[J]. 计算机科学, 2018, 45(4): 157 -162 .
[4] 王欢,张云峰,张艳. 一种基于CFDs规则的修复序列快速判定方法[J]. 计算机科学, 2018, 45(3): 311 -316 .
[5] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 .
[6] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[7] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[8] 刘琴. 计算机取证过程中基于约束的数据质量问题研究[J]. 计算机科学, 2018, 45(4): 169 -172 .
[9] 钟菲,杨斌. 基于主成分分析网络的车牌检测方法[J]. 计算机科学, 2018, 45(3): 268 -273 .
[10] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99, 116 .