近年来面向服务架构(Service Oriented Architecture, SOA)作为一种非常有前景的软件开发技术,已经吸引了越来越多的关注。SOA松散耦合的特性保证了服务的快速组合和动态配置,然而,与此同时也给系统的一致性和可靠性带来了更多的挑战。因此,在模型级上对服务协同的一致性和可靠性的验证逐渐成为研究热点,借此可以大大降低SOA应用的开发风险,节约企业的人力物力。统一建模语言(Unified Modeling Language, UML)已经成为面向对象分析和设计方法的代表,获得了广泛的关注。UML是一种统一的、便捷的而且表达能力强的可视化建模语言,使其成为模型驱动式软件开发过程中的核心技术,而缺乏精确的语义描述又使得UML难以验证设计规范是否满足系统需求。通过对服务协同概念及验证方法的分析,本论文提出了一种基于SPIN模型检测的动态协同服务间一致性的验证方法。首先对UML顺序图进行了状态属性的扩展,增加了消息的进入状态属性,得到扩展顺序图(Extended Sequence Diagram, ESD),增强了UML顺序图面向系统动态行为的表达能力；其次,通过对基于契约的服务协同和ESD语义的分析,形式化分析和描述了服务间的协同时序契约(Collaboration-Contracts, CC)的概念,形式化定义了系统中服务动态行为一致性的概念,为服务间的协同协议提供了形式化支持；然后,选取UML状态图建模服务的动态行为,选取UML扩展顺序图建模服务间的协同时序契约,根据相应的映射规则,将UML状态图建模的动态行为映射成验证工具SPIN的建模语言Promela,将UML扩展顺序图建模的协同时序契约映射成LTL时态逻辑公式；利用模型验证工具SPIN验证映射后Promela模型是否满足LTL时态逻辑公式所描述的系统特性,从而验证服务的动态行为是否满足规定的协同时序契约,确定系统中动态协同服务间的一致性；最后,在上述工作的基础上,设计并开发了模型与验证的集成开发环境tMDA(Trustable Model Driven Architecture),并用tMDA建模和验证了轨道交通中的联锁站仿真系统。