本文研究编排(choreography)语言及其对分布式系统设计的支持。由于分布式系统中成员的自主性和并行性，这种系统的设计和验证非常困难。Web服务即是分布式系统的一种组织形式，它被用于跨组织的业务流程时通常关乎多方的商业利益，保证其正确性和容错性是非常重要的。无论是实际应用还是理论研究，都需要关注这些方面的问题。　　 编排语言是一类新出现的用于设计分布式系统的语言。编排的思想是倡导一种从全局到局部的设计方式：首先用编排的形式设计系统的全局模型，并在这个模型上检验关心的性质；然后从编排自动地或人工地得到各子系统的实现或实现框架；最后完成各个子系统的实现。本文通过对编排语言、验证方法和自动生成技术的研究，对相关工作步骤的有效性的证明，为建立这样一条设计途径提供理论支持。　　 由W3C提出的Web服务编排语言(WS—CDL)，是目前不多的编排语言之一。WS—CDL拥有丰富的语言特性，除了基本的控制流之外，还包括通道传递、异常处理和终结化(Finalization)。本文以这个语言为背景，设计了一系列小的编排语言，基于它们分别讨论不同的语言特性。针对每一类重要的语言特性，文中都完成了几方面的工作：首先定义一个小语言及其形式语义，讨论语言性质：而后定义相应的用以描述子系统实现的编制(orchestration)语言，定义编制语言的语义；然后，定义从编排语言描述自动生成编制语言程序的过程(称为投影过程)。最重要工作的是讨论跟这个语言特性相关的，在分布式系统运行中应该满足的性质，例如：无死锁；怎样在编排上检查这些性质；以及怎样保证从编排投影得到的实现保持了这些性质。　　 具体来讲，本文主要研究了三方面的重要语言特性。　　 一，控制流。包括最基本的顺序复合、并行、选择等控制结构，以及死锁、时序等系统设计中最关心的性质。我们讨论了编排的可实现性，即是否有一组实现跟编排拥有同样的时序性质而且不会死锁。分析了影响可实现性的顺序复合和选择结构，提出了限制编排的语法条件，并证明了满足条件的编排被它的投影实现。　　 二，通道传递。分布式系统的各个部分通过通道相互通信，为了支持动态的系统组合，即允许某些子系统动态地加入到另一些子系统之间已经开始的会话中，子系统之间需要交换通道才能相互通信。因此，Web服务中引入了通道传递机制。针对实现中可能出现的通道缺失、通道错误和通道冗余等问题，本文提出了编排语言中需要提供的语言结构和检查这些问题算法，并证明了通过检查的编排投影后得到的编制系统不会出现上述问题。　　 三，异常处理。由于需要考虑异常协作处理和并发异常，分布式系统中的异常处理过程远比顺序程序复杂。为了处理这些复杂情况，子系统之间需要进行信息交换和同步。本文研究了协作式异常处理的算法，形式化地定义了编制层的运行时支持系统。在此基础上提出了一组子系统需要满足的条件，以确保各子系统在正常运行和异常处理过程中始终保持相互一致。另一方面，文中还研究了编排层面上结构化异常处理的表达方式和投影算法。两项研究相比，编制层子系统需要满足的约束条件非常复杂，而编排几乎不需要特别的限制就能自然地投影生成一致的编制系统。　　 通过对编排语言的几个主要语言特征的分析，及其相应的检查和投影算法的研究，我们证明了满足一定条件的编排总是可以投影生成正确的实现。同时，在讨论的过程中也对现有的编排语言提出了一些意见，为编排语言的设计和从编排语言出发的系统开发方法奠定了理论基础。