面向服务软件异常处理过程的可终止性验证  

Verification of Termination for Exception Handling Process in Service-Oriented Software

作　　者：蒋曹清[1,2] 应时[1] 文静[1] 贾向阳[1] 管华[1] 

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

出　　处：《计算机科学与探索》2012年第3期208-220,共13页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金No.61070012;国家重点基础研究发展规划(973)No.G2007CB310800~~

摘　　要：大规模面向服务软件运行环境的动态性和不确定性使其异常处理逻辑复杂度高,导致异常处理过程的可终止性验证异常困难。而异常处理过程的可终止性是确保其正确性的重要基础,如果异常处理过程不能终止将导致面向服务软件无法正常运行。目前缺乏异常处理过程的可终止性验证方法,从而无法保证异常处理达到预期的目标。基于着色Petri网(colored Petri net,CPN)提出了一种面向服务软件异常处理过程的可终止性验证方法。该方法建立了包括正常流程和异常处理逻辑的异常层次CPN模型(hierarchy CPN model for exception handling,HCPN4EH)。基于此模型验证了异常处理过程的可终止性。通过一个实例说明了该方法的可行性和有效性。得到的可终止性验证结果可为进一步分析异常处理过程的正确性提供基础。The dynamic and uncertainty of large-scale service-oriented software trend to cause high complexity of the exceptions logic which can lead to be extremely difficult to verify the termination of exception handling process. However, the termination of exception handling process is important foundation to ensure its correctness. If the exception handling process does not terminate, service-oriented software will not work normally. The current research rarely focuses on the verification method of termination for exception handling process in service-oriented software, thus exception handling can not be guaranteed to achieve the desired objectives. Therefore, this paper proposes a colored Petri net （CPN）-based verification method of termination for exception handling process in service-oriented software. Firstly, this method establishes the hierarchy CPN model for exception handling （HCPN4EH） including the CPN description of normal flow and exception handling logic. Then, the termination of exception handling process can be analyzed and verified according to the established model. Finally, an example demonstrates the feasibility and effectiveness of this method. The results of termination verification can provide the foundation for further analysis of correctness of the exception handling process.

关 键 词：异常处理 可终止性验证 验证方法 面向服务软件 

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