随着网络的快速发展，单个web服务功能已经不能满足用户需求，需要将多个web服务组合起来，以提供更为强大的功能。目前web服务组合的研究已经取得一定的进展，但还缺乏一个通用的实现框架对web服务的自动操作、自主交互及动态组合进行规范。作为分布式技术和人工智能技术相结合的产物，移动agent技术具有自主行为和动态建模的优势，能够在异构网络中自主地迁移。本文将移动agent技术应用于web服务组合领域，为实现动态web服务组合和异构的互联网软件系统开发提供了一种新的技术途径。结合web服务组合和移动agent技术，本文提出基于移动agent的层次化服务组合模型。主要工作如下：(1)采用高级Petri网建立web服务组合形式化模型文中将整个系统模型分为系统层、agent层以及安全机制层，首先采用高级Petri网对系统层和agent层进行形式化的建模，然后对模型的安全性问题进行讨论，并建立了保护主机的安全机制模型。系统模型清晰表达各个层之间的交互和连接关系，体现移动agent的移动性、智能性和系统层的控制性、灵活性。(2)为了保证模型的正确性，采用形式化的模型验证方法。文中采用主流的模型检测工具SPIN对建立的形式化模型进行验证，具体过程是提出高级Petri网模型到Promela目标模型的具体转换规则，实现模型转换，利用线性时序逻辑公式(LTL)对系统性质进行描述，完成系统的服务交互过程和安全性验证。这种方法可以有效地减小系统验证规模，提高验证效率。(3)结合web信息服务查询系统实例，应用提出的方法对其进行形式化的建模与验证分析。以典型的web信息服务查询系统为例，详细介绍本文所提出方法的实际应用，首先对系统中的各个部分建立了形式化模型，然后采用提出的模型验证方法对系统的主要属性和安全性进行实际验证和分析，说明提出方法的正确性和有效性。