基于模型检测的面向服务软件异常处理可终止性的验证方法  

An Approach of Model Checking Termination for Exception Handling in Service-oriented Software

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

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

出　　处：《小型微型计算机系统》2015年第11期2484-2491,共8页Journal of Chinese Computer Systems

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

摘　　要：针对面向服务软件异常处理的可终止性难以验证问题,提出一种基于模型检测的验证方法.该方法首先基于已建立的异常处理模型和形式定义的异常处理可终止性,使用ASK-CTL(Computation Tree Logic)刻画异常处理的可终止性,然后基于本文提出的异常处理可终止性的模型检测算法,可获得异常处理可终止性验证结果.最后,结合实例从可行性和有效性角度对验证方法进行实证和评估,结果表明,本方法能有效验证异常处理的可终止性,且具有较好的性能,为进一步分析异常处理的正确性提供支持.Aiming at the difficulty of termination verification for exception handling in service-oriented software,a verification approach is proposed to solve the problem based on model check. With the proposed approach,based on the built model for exception handling,and the formal definition for termination of exception handling,the termination of exception handling is specified with ASKCTL（ Computation Tree Logic）,and based on the model check algorithm proposed in this paper to verify the termination of exception handling,the verification result of termination of exception handling can be obtained. A case study is given to confirm and evaluate verification approach of exception handling from feasibility and effectiveness. The results showthat the approach can effectively verify termination of exception handling,and has better performance than traditional approaches,further provide support for correctness analysis of exception handling.

关 键 词：面向服务软件 异常处理 模型检测 可终止性验证 

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