XML标准和面向服务的计算模式(Service-Oriented Computing,SOC)大大降低了跨域协同(Cross Organizational Cooperation,COC)系统的实现难度和实施成本,使多主体协同系统(Multi-Agent Cooperation System,MACS)、虚拟组织(Virtual Organization,VO)和E机构(E Institution)等跨域协同系统的大规模应用成为可能。但是跨域协同系统体系结构的复杂性,组件的分布性和异构性,以及执行过程的异步性使系统验证颇为困难。如何检验实现的系统能否达到预期目标,是否满足一致性、完备性等属性要求是此类系统设计和实现过程中面临的主要挑战之一。测试和形式验证是目前实现系统验证的主要途径。相比之下,传统测试方法由于无法保证测试过程覆盖系统全部执行路径而无法满足要求。基于形式化方法的自动形式验证理论和技术,凭借其严格性、精确性的特征和验证过程自动化的优势,成为目前COC系统验证的最佳选择。由于体系结构上的差异,我们无法设计通用的COC系统验证方案,但是对典型系统验证的研究能够为类似系统验证工作提供方法论上的指导,从而降低验证的实现难度。可信自治式服务协同系统(Trusted and Autonomic Service CooperationSystem,TASCS)是SOC计算模式下的新型可信跨域服务协同平台,涵盖了COC系统研究领域的主要理论和技术,因此其验证研究对于实现其他跨域协同系统验证有很大的参考价值。本文对跨域服务协同和自动形式验证理论和技术进行了深入的研究和探讨,提出了一种基于自动形式验证技术的TASCS验证方案,初步解决了它的验证问题,也为其他COC系统验证提供了有益的借鉴。论文的内容主要包括以下几个方面:首先,论文介绍了模型检验和形式语句判定过程这两种自动形式验证方法体系。讨论了自动形式验证的基本概念、理论、技术和主要验证工具,分析了这两种方法体系的适用性以及应用的约束和限制。其次,论文介绍了ebXML分布式协同理论和规范调控的多主体协同系统理论这两个TASCS的理论基础。前者是TASCS分布式业务流程的参考模型,后者则是TASCS可信机制的理论基础。提出了一种规范调控的多主体协同系统动态模型和基于模型检验的动态属性验证机制,为TASCS验证的实现提供了借鉴和参考。接着,论文提出了一种基于符号模型检验技术的TASCS动态属性验证方案。该方案建立了基于道义逻辑和命题逻辑的形式化规范语言及其状态集语义,通过与系统Kripke结构的结合实现了规范和协同系统动态模型之间的无缝衔接。在此基础上实现的系统动态属性符号模型检验算法解决了TASCS的动态属性验证问题。再次,论文对TASCS分布式业务流程设计和实现过程中面临的一致性问题进行了分析和归类,提出了一种基于形式语句判定过程的分布式业务流程一致性验证方案。该方案用命题逻辑或带未解释函数的等式逻辑语句描述待验证的一致性问题,借助形式语句有效性判定算法实现了对TASCS分布式业务流程一致性问题的验证。最后,论文介绍了医疗卫生领域人体器官/生理组织移植跨域协同系统体系结构,叙述了验证方案在在该系统中的实现过程,讨论了该方案的优点和不足,以及它对类似模型验证的指导意义。