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

Abstract: Interpretation JIANG Cao-qing¹ XIAO Fang-xiong¹ GAO Rong¹ YING Shi² WEN Jing² (Department of Computer and Information Management,Guangxi University of Financial and Economics,Nanning 530003,China)¹ (State Key Lab of Software Engineering,Wuhan University,Wuhan 430072,China)² 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