云制造作为一种新的制造模式,采用云计算思想,利用分布式技术与资源重用技术,为解决制造业“信息孤岛”问题带来了曙光。云制造服务组合形式化建模与验证是确保云制造服务组合顺利执行的关键技术。论文以云制造服务组合为研究对象,以进程代数方法为依托,从理论、模型和应用三个层次上来研究云制造服务组合方法、服务交互场景模型、服务组合过程模型、形式化验证、服务组合平台开发等内容,以促进云制造环境下服务组合的正确性、安全性,帮助云制造服务用户按需获取、付费使用云制造服务,有助于用户在更广的范围里共享和优化配置制造资源,提高制造的柔性、敏捷性和企业竞争力。本文对云制造服务组合、建模及形式化验证的关键技术进行了系统的研究,主要包括:研究了云制造服务组合平台体系架构,详细阐述包括制造资源层、虚拟资源层、服务信息层、核心功能层、终端应用层和服务运营层在内的各层主要功能和实现技术;根据面向服务的理念将云制造资源划分为物质型、知识型和能力型三种制造资源,并分析这三种制造资源的特性,给出了对其进行描述与封装的方法;探讨了云制造资源服务化的实现过程,将其分为资源感知、虚拟封装、服务蜕变、服务展现四个主要环节;建立了云制造资源服务化模型,并给出了机床服务化等实例。研究了基于进程代数、云熵遗传算法与业务智能的云制造平台智能服务组合方法,阐述了智能服务组合方法的基本原理及其三种不同服务组合模式:手动模式、半自动模式和自动模式云制造服务组合方法;提出并分析了云制造服务组合策略;给出了服务匹配度、组合和谐度和云熵的计算方法,并在此基础上构建云制造服务组合多目标优化数学模型;给出了一种求解云制造服务组合多目标优化问题的云熵遗传算法;以自动导引搬运小车制造任务为例,验证了所给出的云制造服务组合多目标优化模型的正确性及其求解算法的可行性。研究了云制造服务组合形式化建模方法,重点阐述了服务交互场景形式化模型和服务组合进程形式化模型。云制造服务交互场景形式化模型用于描述云制造服务间的交互行为,可清晰表达云制造服务组合中各组成部分之间的业务逻辑关系,并可模拟云制造服务组合的整个交互行为;云制造服务组合进程形式化模型用于描述云制造服务的组合活动,可表达云制造服务组合实现的工作流程和工序关系。以MillingMachine服务与MoldFactory服务为例分别验证了云制造服务交互场景形式化建模和组合进程形式化建模方法。研究了云制造服务组合主要属性的形式化验证机制。以进程代数为工具,将服务交互场景模型验证与服务组合进程模型验证相结合;在对服务交互场景模型进行形式化验证时,将整个服务组合的交互行为根据场景分割原理划分为多个服务交互场景,重点验证各服务交互场景的功能属性;在对服务组合进程模型进行形式化验证时,则重点验证各服务组合进程模型中各服务组合活动的非功能属性。研究了机加工云服务平台技术架构与实现工具,阐述了云制造服务组合形式化建模与验证技术在云服务平台中的具体应用。以医用氧气吸入器制造任务为例展示了智能服务组合方法在机加工云服务平台中的具体应用;而以自动导引搬运小车车身加工服务组合和开放式集成制造系统服务组合为例,分别展示了服务组合进程模型和服务交互场景模型的应用,并运用所提出的形式化验证方法对两个应用案例的形式化模型的主要属性进行了验证。案例研究结果表明本文提出的基于扩展进程代数的形式化建模与验证方法是可行的,可验证服务组合相关属性,并且与其它服务组合方法相比较,本文提出的智能服务组合方法满足服务组合的需求项数最多。