编排(Choreography)和编制(Orchestration)是常用于描述合成网络服务的两种方式的语言。前者从一个整体的视角定义了系统中各服务之间的交互，而后者仅从一个服务的角度定义了应调用什么服务以及应该何时调用，没有定义多方如何进行协作。根据两者的特性，在设计服务组合系统时，可以先用编排来定义一个系统高层次上的服务交互协议，再用编制描述具体某个服务的行为以实现编排层定义的协议，最后用流程语言实现整个系统。这种做法的优点是：其一，提供了一种从上至下的实现服务组合系统的方法；其二是能够支持系统的从下至上的一致性的验证。这种系统设计方法的应用需要一个能够描述编排与编制的形式化系统做为依托。本文分析了各种形式化方法的优劣，采用了进程代数范畴内的方法对编排编制进行形式化描述。通过对一个理想的服务组合系统的设计模型的分析，总结了现有解决方案的不足，针对这些不足，本文在语义模型中加入了状态的描述，增强了其表达能力，使其能够描述确定性选择、分支等结构化流程；在系统中引入了三层的结构，分别为进程内部行为、进程间的交互以及服务间的互操作，层次化了交互语义，以利于系统在不同层面上的单独设计；针对目前服务组合系统的不确定性，文中实现了系统状态、服务位置、服务接口以及服务功能的动态性语义，并举例进行了讨论；同时文章还给出了编制形式化系统到WS-BPEL流程的映射及转化算法，有助于以后执行代码的自动生成。文章的最后给出了一个航空公司订票系统的设计过程。分别从编排和编制的角度设计了系统的交互并发行为，根据外部可观察行为一致性原理，分析了错误的编制设计，给出了正确的以及一个精化了的系统模型，同时进行了系统的一致性验证。最后给出了形式化系统到流程语言转换之后的部分代码。