基于服务协调模型的业务事务验证方法  

Business transaction verification approach based on service coordination model

作　　者：袁敏[1,2] 黄志球[1] 李祥[1] 闫艳[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016 [2]湘南学院计算机科学系,湖南郴州423043

出　　处：《计算机集成制造系统》2012年第3期662-671,共10页Computer Integrated Manufacturing Systems

基　　金：国家863计划资助项目(2009AA010307);国家自然科学基金资助项目(60873025);湖南省自然科学基金资助项目(09JJ3114);湘南学院资助科研项目(2007Y029)~~

摘　　要：为有效地保证Web服务业务活动中事务可靠地执行,提出了一种检查伙伴服务之间协调行为一致性的方法。针对长事务给出用Pi-演算建模业务活动中服务协调行为的方法;定义了标号迁移系统和Kripke结构这两种状态自动机之间的语法映射关系,提出了Pi-演算进程模型到符号模型检测工具输入语言的转换方法;在模型检测结果的基础上,用反例引导用户进一步精化模型,以解决业务流程集成中参与者协调一致性问题。通过实例验证了该方法的有效性。To ensure the reliability of transaction execution in Web service business transaction, an approach to check the consistency of coordination actions among partner services was proposed. Aiming at the long-running transac- tions, a rigorous method by using Pi-calculus to calculate the service activities coordination in modeling business was put forward. The syntax mapping of automaton between Labeled Transition System（LTS）and Kripke structure was defined, and transformation from Pi-calculus process model to imput language of symbolic model checking was pro- posed. On the basis of test result, a counter-example was used to refine the model. Therefore the coordination prob- lem of participants in business process integration was solved. The example was used to verity the effectiveness of proposed method.

关 键 词：业务流程集成 长事务 服务协调 PI-演算 形式化验证 WEB服务 

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