近年来,以Web服务为基本构件的面向服务计算(SOC)得到越来越广泛的关注,将发布的单个服务组合成更强大更可靠的系统能够进一步发挥SOC的优势,因此服务组合与验证一直是Web服务研究领域的热点和难点。服务组合的形式化语义描述能够支持组合正确性的验证和测试,但已有服务组合形式化研究主要对服务组合交互行为进行建模和验证,缺乏对服务组合功能正确性的关注。本文在扩充已有面向服务代数规约描述语言基础上,提出一种基于代数规约的服务组合形式化描述方法,对组合抽象功能和交互行为进行形式化描述,为服务组合的可验证性和可测试性奠定了理论基础。本学位论文主要包括以下三个方面的工作:1.为更好地描述服务组合,扩充现有的面向服务系统代数规约描述语言SOFIA,进一步增强语言的服务描述能力和模块化特性。首次完整地给出扩展后SOFIA语言的语法及其形式化定义,并基于JavaCC设计和实现SOFIA语言的解析器,检查面向服务系统代数规约的语法正确性和类型正确性,并将解析结果存入数据库以供后期测试使用。2.针对已有面向服务系统的代数规约并未描述组合实现过程的问题,提出一种面向服务组合的代数规约方法,引入了规约包机制以支持该方法。当多个服务组合在一起时,以这些服务的代数规约包为基础,一方面抽象地定义组合服务的交互过程和语义,形成描述服务组合实现方式的实现规约包,另一方面抽象地定义组合服务对外接口及其功能语义,形成描述组合服务需求的抽象规约包。在实现规约和抽象规约的双元结构基础上,进一步定义了实现规约和抽象规约之间所必须满足的“实现”关系,阐述了满足实现关系可以保证实现的正确性这一结论的证明思路,从而为服务组合的可验证性和可测试性奠定了理论基础。在此基础上,设计和开发证明实现关系是否成立的辅助推导工具。3.将面向服务组合的代数规约方法应用于若干系统进行案例研究,用SOFIA语言对被组合服务和组合服务进行规约,并证明案例中组合实现的正确性。最后分析阐述用代数规约描述服务组合的抽象性、可表达性和可验证性。