计算机科学与探索 ›› 2012, Vol. 6 ›› Issue (3): 208-220.DOI: 10.3778/j.issn.1673-9418.2012.03.002

• 学术研究 • 上一篇    下一篇

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

蒋曹清1,2+, 应 时1, 文 静1, 贾向阳1, 管 华1   

  1. 1. 武汉大学 软件工程国家重点实验室, 武汉 430072
    2. 广西财经学院 信息与统计学院, 南宁 530003
  • 出版日期:2012-03-01 发布日期:2012-03-01

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

JIANG Caoqing, YING Shi, WEN Jing, JIA Xiangyang, GUAN Hua   

  1. 1. State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072, China 2. College of Information and Statistics, Guangxi University of Financial and Economics, Nanning 530003, China
  • Online:2012-03-01 Published:2012-03-01

摘要: 大规模面向服务软件运行环境的动态性和不确定性使其异常处理逻辑复杂度高, 导致异常处理过程的可终止性验证异常困难。而异常处理过程的可终止性是确保其正确性的重要基础, 如果异常处理过程不能终止将导致面向服务软件无法正常运行。目前缺乏异常处理过程的可终止性验证方法, 从而无法保证异常处理达到预期的目标。基于着色Petri网(colored Petri net, CPN)提出了一种面向服务软件异常处理过程的可终止性验证方法。该方法建立了包括正常流程和异常处理逻辑的异常层次CPN模型(hierarchy CPN model for exception handling, HCPN4EH)。基于此模型验证了异常处理过程的可终止性。通过一个实例说明了该方法的可行性和有效性。得到的可终止性验证结果可为进一步分析异常处理过程的正确性提供基础。

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

Abstract: The dynamic and uncertainty of large-scale service-oriented software trend to cause high complexity of the excep-tions 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 fea-sibility and effectiveness of this method. The results of termination verification can provide the foundation for fur-ther analysis of correctness of the exception handling process.

Key words: exception handling, termination verification, verification method, service-oriented software