面向服务计算(Service-Oriented Computing,SOC)是一种新的计算范型,SOC在流程描述、数据管理以及分布式计算中间件技术的基础上,提出以服务作为构建软件的基本单元。SOC希望通过统一的技术规范,来达到网络资源的充分利用和共享,从而提高IT企业应对需求的能力和工作效率。服务接口是SOC中服务使用者关于一个服务所能够得到的唯一信息,准确而且充分的服务接口描述是保证SOC中服务查找、服务组合等关键操作质量的重要因素。因此,如何保证接口描述的准确性,如何在服务接口描述中包含多方面的服务信息成为SOC中的关键问题。形式化方法基于严格的数学理论来提供系统的描述和分析方法,不仅能够消除系统建模过程中的不准确或歧义性,而且还能通过形式化验证来保证系统的正确性,提高系统的质量。本文希望通过研究形式化的服务接口模型及验证方法,来保证服务接口的准确性。事务是SOC中保证系统正确性和一致性非常重要的手段,SOC中的事务往往执行时间较长,需要与不同的服务提供组织协商完成,与传统事务相比,SOC中的事务对原子性和隔离性的要求相对松弛,因此SOC中一般使用长事务模型来完成具备事务要求的任务。本文针对具备长事务特征服务的接口描述,在Beyer等人提出的Web服务接口理论的基础上,提出了支持长事务行为特征描述的多层接口模型,能够分别在特征、会话和协议三个层次描述支持后向恢复长事务机制的服务在接口层面的动作引发关系。在每层接口模型的基础上,给出了基于接口的服务相容性和可替换性的检查方法。此外,为了保证服务接口的正确性,分别在三个层次给出了服务接口关键性质的规约方法和相应的验证方法。为了支持日益复杂的业务逻辑,出现了更加灵活的长事务模型,并且在目前主流的服务编制语言中都得到了体现。针对目前长事务模型中的前向恢复、事务嵌套以及可订制错误处理这些特征,本文提出了扩展协议接口来描述具备这些特征的服务接口。基于时序逻辑,给出了一般化的协议接口关键性质的规约方法,通过扩展协议接口的操作语义,采用模型检验这种形式化技术来验证扩展协议接口是否满足协议规约。为了应用扩展协议接口及验证方法,本文针对使用Web服务业务流程执行语言(BPEL)实现的服务,给出了从BPEL程序中提取扩展协议接口的方法,并使用验证方法对提取的扩展协议接口进行验证。在扩展协议接口、提取方法以及验证方法基础上,给出了它们在BPEL程序基本开发过程中的应用方式,从而可以在开发过程中验证BPEL程序,提高使用BPEL实现服务的质量。服务构件作为提供服务的计算实体,是SOC中服务提供方在服务开发过程中需要构建的主要单元。如何在开发过程中设计服务构件并保证服务构件的可靠性是提高服务质量、保证面向服务系统正确性的关键问题。与服务接口类似,本文希望通过研究形式化的服务构件建模技术以及精化方法,并在目前主流的模型驱动以及形式化验证技术基础上,寻求严格的服务构件设计方法,来提高服务构件的可靠性。本文在何积丰等人提出的构件以及对象精化理论的基础上,针对目前SOC中服务的异常行为,提出了支持异常信息描述的接口契约模型,可以支持服务接口的功能规约、服务使用方式以及异常信息多个方面的描述,并给出了不同方面行为的一致性条件,以及接口契约的数据精化方法。针对服务构件实现层面的事务特征,提出了支持补偿恢复机制的服务构件实现模型,并给出了服务构件相容性的定义。针对具备事务特征的应用,提出了支持后向恢复长事务描述的进程构件模型,用于服务构件之间的复杂组合。服务构件理论为服务构件的设计提供了理论基础,支持从接口契约到构件层面的精化,为进一步的应用形式化验证技术提供了前提。在服务构件理论的基础上,本文研究了严格的服务构件设计方法,受关注点分离(Separation of Concerns)设计思想启发,在现有模型驱动、面向对象以及面向构件理论和技术的基础上,提出了迭代以及增量式的模型驱动的服务构件设计方法,其中包括需求建模、功能设计、逻辑构件设计以及详细设计四个阶段,在每个阶段使用服务构件理论中提供的建模元素对服务构件进行建模,基于精化理论给出了服务构件设计过程中的精化方法,同时在不同的阶段使用相应的形式化验证技术保证系统模型的正确性和一致性,从而提高了服务构件的可靠性。本文最后设计并实现了接口模型的检查工具,可以对文本格式的多层接口描述进行检查和验证,同时把扩展协议接口的验证嵌入到开源的BPEL设计工具中,可以在BPEL设计过程中对其进行验证。此外,本文还设计并实现了服务构件设计工具原型,支持服务构件设计过程中的图形建模、静态和动态一致性检查、基于文本模型的自动精化等主要设计活动。