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 ex-ception 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 fea-sibility and effectiveness of this method. The results of termination verification can provide the foundation for further analysis of correctness of the exception handling process.%大规模面向服务软件运行环境的动态性和不确定性使其异常处理逻辑复杂度高,导致异常处理过程的可终止性验证异常困难.而异常处理过程的可终止性是确保其正确性的重要基础,如果异常处理过程不能终止将导致面向服务软件无法正常运行.目前缺乏异常处理过程的可终止性验证方法,从而无法保证异常处理达到预期的目标.基于着色Petri网(colored Petri net,CPN)提出了一种面向服务软件异常处理过程的可终止性验证方法.该方法建立了包括正常流程和异常处理逻辑的异常层次CPN模型(hierarchy CPN model for exception handling,HCPN4EH).基于此模型验证了异常处理过程的可终止性.通过一个实例说明了该方法的可行性和有效性.得到的可终止性验证结果可为进一步分析异常处理过程的正确性提供基础.
展开▼
