论文部分内容阅读
Web服务正从最初关注描述、发布和交互向支持健壮的业务协作新阶段发展，BPEL作为Web服务业务流程执行语言成了服务组合和业务流程正确性验证研究的焦点，BPEL语言的设计目标是描述由一个组织机构执行的单个业务流程，缺乏对多方服务参与者协调一致性的描述能力，这些研究没有提供参与者之间协调事务的建模与验证方法，如何保证Web服务组合和业务流程的参与者之间协调一致性是亟待解决的重要问题．在Web服务事务规范WS-TX中参与者之间的消息通信缺乏严格的语义，无法精确地描述复杂的协调活动，本文首先对消息通信进行形式化描述，用Pi-演算建立了服务协调的行为模型，并基于等价自动机转换的模型检测方法，提出了Pi-演算移动进程模型到符号模型检测工具输入语言的转换方法，在模型检测反例分析方法上给出了Pi-演算进程形式的反例生成算法，用易理解的反倒状态变迁路径图的方式反馈给业务流程设计者进行修改．从建模、转换、验证到分析，该方法能自动检查分布式业务流程设计的正确性，有效地确保业务事务执行的可靠性和一致性．