Web服务技术自上世纪90年代诞生以来,就开始了需求激励技术、技术推动服务的浪潮式发展。在信息技术推陈出新日益频繁的今天,REST架构由于具有简单性、高可扩展性、高可伸缩性、低耦合性、高可重用性等特性,引起了理论界和工业界的瞩目,对它的研究和应用也越来越多。RESTful Web服务是指将REST架构应用在Web中,以资源为中心,使用URI作为统一资源标识符,使用HTTP协议中的方法作为操作资源的统一方法的Web服务。从REST架构提出至今,形式化领域中对其的研究工作并不多,而缺少形式化模型的支持使得REST架构风格的设计原则在工业界经常被误用,REST也没有发挥出它真正的强大能力。本文使用进程代数中的CSP对RESTful Web服务进行建模与分析。首先对REST架构本身以及RESTful Web服务进行了形式化建模,前者关注各个模块内的构成,后者关注模块之间的交互。RESTful Web服务模型将整个服务抽象成客户端、服务器、资源三个模块,分别描述成CSP中的进程。每个模块结合HTTP协议中的方法,对发送请求和接受请求的行为进行刻画,分别描述了各个方法的具体行为。通过将资源独立描述成一个进程,模型很好地刻画了资源的状态变化。本文还使用一阶逻辑对RESTful Web服务中最重要的无状态性、超媒体驱动以及HTTP协议方法的安全性和幂等性进行描述,然后使用模型检测工具PAT对其进行了验证。最后,本文使用了一个具体案例来说明模型的适用性。运用形式化方法对RESTful Web服务进行建模与分析,能增强工业界对REST架构相关概念的理解,同时对其性质的描述提供了一个检验Web服务是否为RESTful的方法。