摘要: 本文讨论模型检验技术及其在Web服务编排中的应用。 Web服务编排从全局角度描述Web服务组合。编排的最基本行为是两个参与方之间的一次交互，编排将涉及到多个参与方的各种交互按照顺序、并行、非确定选择、条件选择、迭代等控制结构组合起来，协... 展开 本文讨论模型检验技术及其在Web服务编排中的应用。 Web服务编排从全局角度描述Web服务组合。编排的最基本行为是两个参与方之间的一次交互，编排将涉及到多个参与方的各种交互按照顺序、并行、非确定选择、条件选择、迭代等控制结构组合起来，协同一道完成某种任务。交互在通道上进行，为了支持动态变化的互联拓扑，编排引入了通道传递机制。随着参与方的增多、控制结构的复杂化、再加上由通道传递引起的动态性，这些都使得编排的正确性难以保证。 模型检验技术为验证编排的正确性提供了可能。模型检验的目标是证明模型满足其规范，它针对的模型是有穷状态转换系统，模型规范一般采用时态逻辑表达。模型检验技术面临的主要挑战，是状态空间爆炸问题。为应对此挑战，建模中的抽象技术是最重要的手段之一。 本文将抽象技术与模型检验相结合，针对编排程序，给出一个通用验证框架。该框架由下面几部分组成： （1）以时态逻辑公式表达编排要验证的性质； （2）基于待验证的性质，定义编排中交互的抽象语义，抽象语义用一对前、后条件表示，前、后条件中只保留与待验证性质相关的变量； （3）设计一个组合式翻译过程，该过程可将编排语言中各种控制结构翻译成模型检验工具支持的模型描述语言对应的语句结构。 将这几部分相结合，可以完成对各种复杂编排程序的翻译，翻译后得到的模型描述与待验证的时态公式一道交由模型检验工具验证。整个翻译过程是半自动的（因为抽象语义的定义需要人工参与）。通用验证框架可以由多种模型检验工具来具体实现，本文采用两种典型的模型检验工具SPIN和NuSMV分别实现了该框架。 本文基于该框架验证了编排的一些重要性质，这些性质包括编排无通道缺失、编排无通道冗余、编排的一次性通道无错误使用。在编排有通道缺失时，在不改变编排控制结构的前提下，通过在一些执行路径的交互上增加通道传递可能实现对通道缺失的修补。采用通用验证框架提供的方法，可以辅助完成这样的工作，即：找到能用于修补通道缺失的执行路径。对一些不能以此种方式修补的编排（称为存在固有缺陷）可以成功地做出识别。 编排语言的基础思想是以全局角度描述多方参与的交互过程，这一思想显然可以推广到更一般的分布计算环境（不限于Web服务组合）。对资源访问的处理是分布计算环境要考虑的关键问题，本文以通道来表示资源访问许可，以通道类型表示资源访问类型，以支持带类型通道的编排语言来描述一般的分布计算模型（尤其是那些与分布资源访问有关的模型）。在此基础上，前面给出的编排通用验证框架完全可以应用到一般的分布计算模型的性质验证上。本文以哲学家就餐问题为例，演示了编排语言对此类问题的表达能力，以及通用验证框架对此类问题的证明能力。 模型检验的全过程包括构建模型、以时态逻辑表达模型规范、最终验证模型满足规范。模型检验问题本质是数学问题，它与模型的表示、与时态逻辑的语义定义、可满足性密切相关。深入理解技术背后的理论对从事模型检验的研究与应用都是有益的。本文从模型、规范、检验算法、工具几方面，尝试对模型检验技术给出全面的、但尽可能简要的描述。在附录中，还对LTL的显式模型检验算法给出了C++的实现。 收起