万维网诞生于1994年,如今已渗透到人们生活的方方面面。一种为高效地开发大规模分布式超媒体系统而提出的、被称为表述性状态转移(REST)的软件架构风格,是万维网获得成功的主要原因之一。REST架构风格从提出至今已有十余年,但是到目前为止,对它进行形式化建模分析的研究工作很少。缺乏形式化模型的支持导致REST的相关概念在工业界屡屡被误解和误用,这阻碍Web架构和Web工程的发展。本文在前人相关工作的基础上,主要考察了REST架构风格中的四个约束条件,分别是客户-服务器约束、分层约束、无状态约束和统一接口约束。我们使用π演算对REST系统进行形式化建模分析,力图在模型中刻画重要的REST约束条件,最终得到一个符合REST架构风格的系统模型。在本文中我们使用了自顶向下的系统建模方法,首先从整个系统中识别出系统组件,然后根据组件的功能划分模块,最后将REST系统的组件和模块抽象为相应的进程,将组件及模块间的消息通信映射为π演算的进程通信,将模块内部数据状态的变化抽象为对相应的数据结构的操作结果。最终,所有模块的进程并发构成了整个系统的形式化模型。最后结合实例详细分析REST的主要约束条件在模型中的刻画情况,阐明了所建立的模型是符合以上枚举的REST的四个约束条件的。我们相信在本文中建立的形式化模型对于增加相关人员对REST的理解、消除对它的误解和误用有所帮助,并相信该模型能用于指导包括Web系统在内的分布式系统软件的开发。