基于CPN模型的REST服务架构标准特征验证方法研究*

赵玉强,刘 靖

(内蒙古大学计算机学院，内蒙古 呼和浩特 010021)

1 引言

2000年,Fielding[1]在其博士学位论文中首先提出REST(REpresentational State Transfer)服务架构，是指一种结合超文本传输协议HTTP(Hyper Text Transfer Protocol)标准和统一资源标识符URI(Uniform Resource Identifier)标准的设计原理抽象成的新风格，其面向资源并强调以资源为中心。当前REST服务架构在企业中应用越来越广泛，很多Web应用系统都是基于REST服务架构研发的，例如Amazon购物网站和Google搜索引擎等[2]。REST服务架构的优点包括：浏览器作为客户端，这样可以简化软件需求；利用缓存机制提高访问速度；通信的无状态性可以让不同服务器处理一系列请求中的不同请求，提高服务器可扩展性；降低Web系统开发的复杂性，提高系统的可扩展性等。

当前也有一些应用REST服务架构的Web应用系统不遵循REST服务架构标准特征约束，故带来相应的诸多问题。比如，不满足无状态约束会破坏系统的可伸缩性，会影响系统负载均衡；不满足客户端服务器约束会增加系统服务器的开销，增加响应时间；不满足可缓存约束会带来更多的时间开销，因为每次调取资源都需向服务器请求，故会增加时间开销等[3]。因此，为防止以上问题的出现，在设计基于REST服务架构的Web应用系统时，需要对该系统设计是否满足REST服务架构标准特征进行验证，以提升基于REST服务架构的Web系统的研发质量。

目前针对REST服务架构标准特征验证的形式化验证方法，主要包括基于有限状态机和CSP (Communicating Sequential Processes)等方法。在基于有限状态机模型的验证中，不支持分层和缓存确认，而使用CSP方法抽象程度较高，描述更加复杂。因此，鉴于CPN(Colored Petri Nets)模型在可视化和层次化建模、复杂数据描述、并发行为描述和动态执行等方面的优势和广泛应用[4 - 6]，本文提出一种基于CPN模型的REST服务架构标准特征验证方法，首先，对REST服务架构的标准特征约束进行CPN建模，包括客户端-服务器约束(Client-Server Constraint)、可缓存约束(Cacheable Constraint)、无状态约束(Stateless Constraint)、分层约束(Layered Constraint)、统一接口约束(Uniform Interface Constraint)等；其次，实现基于模型状态空间执行路径同步匹配的验证，即以应用系统的CPN模型和标准特征约束的CPN模型为基础，对模型状态空间中的各自执行路径进行同步匹配，若路径可同步执行完毕，则说明该应用系统满足该REST服务架构标准特征约束。文中以自行研发的基于REST服务架构的课程管理Web系统为例，验证上述验证方法的可用性和有效性，实验结果表明，本文所提验证方法可以有效确认基于REST服务架构的Web应用系统设计是否符合REST服务架构的标准特征约束，并在不符合标准特征约束时提供直观、可行的执行数据，便于后续完成应用系统设计缺陷定位及修正。

2 相关工作基础

2.1 REST服务架构的基本概念

REST架构以资源为中心，资源是REST架构中最关键的抽象概念，任何单元都可以成为资源。同时所有资源要有统一的资源标识符，使用URI作为资源标识符，对资源的操作不会改变资源标识符，并且所有的操作是无状态的。RESTful Web服务主要使用HTTP协议中的四种方法，包含POST、GET、PUT和DELETE方法。其中，POST方法是新增数据，即新增一个没有ID的资源；GET方法是对数据进行读取，获取一个已有资源；PUT方法是对数据进行更新，更新一个资源或新增一个没有含ID的资源，用给定的表述信息替换资源的当前状态；DELETE方法是删除一个资源，并且删除请求有一个重要的属性，它是幂等的。所谓幂等，就是发送多次请求对资源状态的影响和发送一次请求的影响是一样的[7]。

REST架构主要元素包含数据单元、连接器和组件。其中，数据单元主要由资源、资源标识符、表示符、表示元数据、资源元数据和控制数据组成。连接器作为统一接口用于各组件相互通信和访问资源，主要由客户端、服务器、缓存、解析器和通道组成，连接器封装了资源的底层实现和沟通机制。组件主要包括用户代理、源服务器和中间件，根据他们在应用程序中发挥的作用划分角色。

2.2 CPN方法概述

本文使用CPN技术对REST服务架构进行建模，实验工具为CPN Tools，可以有效支持模型的验证分析。CPN是一种形式化建模方法，由传统的Petri网演变而来，是一种高级Petri网。同时CPN具有很强的数学建模能力，与数学密切相关，常用于对复杂、并发系统的建模分析。CPN建模语言具有一个兼具语法和语义的数学定义。验证方法涉及数学公式属性和计算机辅助证明，该属性由模型实现。

本文使用的CPN检验方法包含如下两种：模拟(Simulation)执行检验方法和状态空间(State Space)检验方法。模拟执行检验方法通过对应用系统建模，验证系统每一步的状态变迁，检验系统模型是否满足预期[8]。状态空间检验方法通过对系统模拟执行后生成相应的状态空间，该状态空间即系统的可执行路径，即CPN模型的所有可达状态和状态变化情况，并将其通过有向图表示出来，其中，节点表示状态，弧代表发生的事件，状态空间可以自动生成。本文使用CPN方法对REST服务架构应用建模，通过状态的变迁模拟应用服务的资源变化，可有效对其进行验证。

CPN使用九元组CPN=(P,T,A,∑,V,C,G,E,I)[9]来表示，各元素定义如表1所示。本文使用的CPN方法严格按照标准来定义。

Table 1 Definition of CPN elements表1 CPN元素定义

2.3 相关工作

文献[7]提出了一种评估REST架构的方法、工具和指导法则，并在ATAM(Architecture Trade off Analysis Method)场景下对该方法进行评估，综合考虑多种属性，验证该方法的正确性。

文献[10]主要使用CSP方法对REST架构进行形式化建模，该方法首先对资源的调用过程进行分析，抽象出四个主要进程组件，包含用户代理(User Agent)、中间件(Intermediary)、源服务器(Origin Server)和资源(Resource)，并表示出四个进程的通信。其次，对基于程分析工具包PAT(Process Analysis Toolkit)模型检验工具和时序逻辑描述对REST服务架构的标准特征约束进行分析和验证。文献[11]同样使用CSP方法对RESTful Web服务进行建模与分析，将REST架构模型抽象成客户端、服务器和资源三个模块，用CSP描述REST架构中的进程及其具体方法行为，使用一阶逻辑对Web服务的无状态等属性进行描述，并基于PAT工具进行验证。此外，文献[12]使用层次CPN对Web Services系统模型进行行为模拟，并基于生成的状态空间完成功能验证，主要是证明Web Services扩展模型可以提高信息的通信传输性能。通过以上研究可知，使用CPN模型对Web应用系统进行建模、分析和验证是可行的。

综上，目前对REST服务架构标准特征的验证研究工作主要集中在基于CSP的方法上，但这类验证方法抽象程度较高，描述较为复杂。本文充分利用CPN建模技术的优势，提出一种基于CPN模型的REST服务架构标准特征验证方法，可以有效确认基于REST服务架构的Web应用系统设计是否符合REST服务架构的标准特征约束，并在不符合标准特征约束时提供直观、可行的执行数据，便于后续完成应用系统设计缺陷定位及修正。

3 REST服务架构标准特征的CPN建模

3.1 REST服务架构的进程视图

由于REST服务架构很强调资源的调用过程，一切以资源为中心，故REST服务架构的进程视图用来对REST架构资源交互进行描述，表示出不同组件之间的交互关系。参考文献[8]的描述，图1给出了REST服务架构进程视图中四个主要组件的交互示例。

Figure 1 Four main parts of the REST service architecture application model图1 REST服务架构应用模型的四个主要部分

REST服务架构的进程视图主要包含用户代理、中间件、源服务器和资源四个组件，组件之间的交互通过通道和接口进行，且都有统一接口，用户代理、中间件和源服务器有内部缓存机制[8]，相互间的通道在图中描述为CHIOS、CHOSR和CHUAI等，实现基于通道机制的信息发送与接收。

具体而言，用户代理(即客户端)发送请求消息时，首先请求其内部缓存以得到资源，若存在其内部缓存中则直接返回给用户代理。若其内部缓存不存在该资源，那么就需向外部网络中间件发送请求消息。这里定义两者之间的内部通道为CHUAI。请求消息可以描述为四元组(GET,PUT,POST,DELETE)，所有消息都以同样的四元组形式表示，该四元组内元素的具体含义参见2.1节描述。中间件主要由代理(Proxy)或网关(Gateway)组成，也有缓存功能。中间件的主要目的是转发消息和传输信息。用户代理向中间件发送请求信息，中间件有两种方式查询资源，一种是向其内部缓存Cache请求资源，另一种是向源服务器请求资源，这里通过内部通道CHIOS进行通信。用户代理需要的资源都存储在源服务器上，源服务器是唯一可以与资源通信的组件。用户代理可以通过中间件与源服务器进行通信，源服务器收到请求资源信息后，先检查其缓存，如果其缓存没有该资源，则源服务器将请求信息发送给资源，并将请求资源返回给中间件。源服务器与资源之间的通信通过CHOSR通道进行。

3.2 基于CPN模型的REST服务架构标准特征约束建模

3.2.1 客户端-服务器约束

用户代理和源服务器作为两个独立的组件，通过统一接口将它们分离。客户端服务器约束对REST架构应用C/S架构特征进行规范，即REST是一种典型的 C/S架构，该约束保证通信只能由客户端单方面发起，表现为请求-响应的形式。REST架构强调瘦服务器端，服务器端只处理跟资源相关的操作，所有显示工作都应该在客户端。用户代理向其内部缓存或源服务器发送请求资源信息，忽略资源不存在的情况，用户代理请求的信息必须存在于其内部缓存或源服务器中，用户代理发出的所有请求消息，都会得到其缓存或源服务器的回复。

图2给出了REST服务架构中客户端服务器标准特征约束的CPN模型。首先，用户代理即客户端发出请求资源信息msg，msg描述为Msg1类型的变量，该类型在CPN建模中描述为record预定义类型：colsetMsg1=recordm:MSG*f:FORMAT*s:SENDER*r:RECEIVER，其中四个元素均为String字符串类型，MSG描述请求资源的内容，FORMAT描述请求资源的格式，SENDER描述请求消息发出者，RECEIVER描述响应消息的发出者。其次，查询用户代理的缓存中是否存在该资源信息，若该资源在其缓存中(用通道请求RequestUserAgent-Cache简称RequestUC变迁出弧表达式中的第一个元素分量m="1"来示例)，则由其缓存返回响应信息给用户代理；若其缓存中不存在该请求资源(用RequestUC变迁出弧表达式中的第一个元素分量m="no"来示例)，则需要去源服务器中再次请求资源。最后，把客户端请求的资源信息返回给用户代理。

Figure 2 CPN model of client-server constraints图2 客户端-服务器约束的CPN模型

3.2.2 可缓存约束

用户代理、中间件和源服务器均具有缓存机制，请求资源信息可以被保存在相应的内部缓存器中，可改善无状态特性带来的低效性。可缓存约束用来检验用户代理、中间件和源服务器是否均具有缓存功能，响应信息可保留在这三个内部缓存中，可缓存属性有效提高了访问性能，缩短系统响应时间，为用户代理带来便利。本文只考虑可缓存的请求信息。如果用户代理首次发送请求信息，则缓存中不存在任何信息，故应向源服务器请求资源信息。否则，用户代理可能直接从其内部缓存中获得资源，无需访问服务器。如果两个请求资源信息功能相同，则第二个可直接访问缓存获得资源信息。

Figure 3 CPN model of cachable constraints图3 可缓存约束的CPN模型

图3给出了REST服务架构的可缓存标准特征约束模型。首先，用户代理发出请求资源信息，该请求资源信息msg描述同上节。其次，查询用户代理的缓存中是否存在该资源信息，若资源存在其内部缓存中(用通道请求RequestUserAgent-Cache,简称RequestUC变迁出弧表达式中的第一个元素分量m="1"来示例)，则由其内部缓存直接返回信息给用户代理；若用户代理的内部缓存中不存在该请求资源(用RequestUC变迁出弧表达式中的第一个元素分量m="no"来示例)，则需要向网络中间件(Intermediary)继续发送请求信息，若存在其缓存中(用通道请求RequestUserAgent-IntermediaryCache,简称RequestUIC变迁出弧表达式中的第四个元素分量r="Ucache"来示例)，就把资源信息返回给用户代理；若中间件缓存中不存在该请求资源信息(用RequestUIC变迁出弧表达式中的第四个元素分量r="Icache"来示例)，则需要向源服务器发送请求信息，若源服务器缓存存在该资源信息(用通道请求RequestUserAgent-ServerCache，简称RequestSC变迁入弧表达式中的第四个元素分量r="Icache"来示例)，则返回给用户代理。最后，若源服务器缓存中不存在该资源信息(用RequestSC变迁入弧表达式中的第四个元素分量r="Scache"来示例)，需要向数据源请求信息，最终返回响应消息给用户代理。

3.2.3 无状态约束

REST服务架构中的服务器端不保存任何与客户端的会话状态信息。所有状态信息只存在通信消息中，即用户代理发送到服务器的请求消息必须包含理解该消息的所有信息。无状态指会话状态信息保留在用户代理中，服务器是无状态的，如果请求信息同时来自不同的用户代理时，但多个用户代理的请求资源信息相同，则源服务器将反馈给用户代理相同的资源信息。REST服务架构的状态指客户端的状态，每个资源在客户端的表述就是客户端的一个状态。状态信息可描述为三元组(id，data，oper)形式，id是指资源标识符的id，data是指资源信息内容，oper是指具体的操作，即GET、PUT、POST和DELETE等操作。

图4给出了REST架构的无状态标准特征约束模型。首先，两个用户代理之间的通信内容都包含在请求信息中，并且用户代理只保存两者的通信内容。其次，用户代理通过通道Request向源服务器发送请求资源信息，然后返回给用户代理。若多个用户代理请求的资源信息相同时，得到的响应信息也必须是一致的(两个用户代理得到的响应信息均为{m="1",f="2",s="3",r="4"})，则表明该REST架构的服务器是无状态的。

Figure 4 CPN model of stateless constraints图4 无状态约束的CPN模型

3.2.4 分层约束

分层约束检验REST服务架构Web应用是否符合三层架构特性，分层约束提高了各层之间的独立性和系统的可伸缩性。在REST服务架构Web应用系统中，组件只能和其邻接组件通信，即用户代理若想发送请求信息时，只能发送给其内部缓存或者中间件，不能直接发送给源服务器，同样源服务器也不能直接返回响应消息给用户代理，该约束将REST架构分解为若干等级的层，其他组件之间的通信也相同。在分层约束条件中，REST架构只考虑三层REST应用系统，即用户代理层、中间件层和服务器层。

图5给出了REST架构的分层标准特征约束模型。

Figure 5 CPN model of layered constraints图5 分层约束的CPN模型

首先，该REST架构是标准的三层架构应用。其次，用户代理只能向中间件发出请求资源信息(用户代理和中间件两者的交互通过通道CHUAI进行)，然后中间件继续向源服务器发送请求信息(中间件和源服务器两者的交互通过通道CHIOS进行)，最后把请求的资源信息再逐步通过以上的接口返回给用户代理。其中，由通道CHUAI和通道CHIOS将三个组件分为三层模型。

3.2.5 统一接口约束

统一接口约束检验组件间通信消息格式是否一致，即检验REST架构应用的接口是否一致，该约束可改善系统的交互性和可重用性。在该约束条件中，体现在用户代理发送的请求消息和源服务器返回的消息格式必须是一致的，即资源的标识符是一致的。请求消息描述为四元组表示{msg,r_format,sender,receiver}，其中,msg表示请求的资源，r_format表示资源的格式，sender表示资源的请求发送者，receiver表示资源的请求接收者。

图6给出了REST架构的统一接口标准特征约束模型。表明用户代理向源服务器发送的请求信息和服务器的响应信息格式是一致的(用Reply变迁出弧表达式中的第一个元素分量m="1"来示例)，发送者和接收者的信息应该具有相同的资源标识符，这体现出REST架构的统一接口标准特性。

Figure 6 CPN model of uniform interface constraints图6 统一接口约束的CPN模型

4 REST服务架构标准特征验证方法

本节提出一种基于CPN模型的REST服务架构标准特征验证方法，以应用系统的CPN模型和标准特征约束的CPN模型为基础，对模型状态空间中的各自执行路径进行同步匹配，若路径可同步执行则说明该应用系统满足该REST标准特征约束。若不符合标准特征约束时，提供直观、可行的执行数据，便于后续完成应用系统设计缺陷定位及修正。

4.1 验证方法的基本思想

本文所提验证方法的核心思想可概述为：构建应用系统的CPN模型和标准特征约束的CPN模型，分别生成各自的状态空间，得到各模型相应的执行路径集合。执行基于模型状态空间的同步路径匹配算法，逐个检验应用系统模型的状态空间执行路径是否同步包含标准特征约束模型的路径，若包含，则验证成功；否则存在不符合之处，通过状态差集定位应用系统模型及系统设计中的缺陷错误，找出不符合的状态和路径，对其进行修改完善，使其满足REST服务架构标准特征约束。

具体而言，执行基于模型状态空间的同步路径匹配算法是核心。首先，我们给出一个核心概念，即同步节点。若REST服务架构标准特征约束模型状态空间的一个节点使用M*来标识，应用系统模型状态空间的一个节点使用M标识，如果M*的Marking值和M的功能等价，即两个节点标记中的关键字段数据相同，并且后续可执行变迁描述的功能也相同，则这两个节点可互称为同步节点。状态空间执行路径的同步包含是指同步节点和变迁路径的包含关系，并且同步节点和变迁路径的执行顺序也要一致有序。算法的关键部分就是其中的状态空间执行路径完成同步执行匹配，直观而言，从状态空间执行路径生成的角度分析，由应用系统模型的初始状态开始执行可能的点火变迁，在经过一个或多个变迁点火后，得到与标准特征约束模型起始节点可同时执行的同步节点；然后，点火同步节点，执行一步操作后，应用系统模型又可能经过一个或多个变迁点火，再次得到与标准特征约束模型起始节点可同时执行的下一个同步节点；依次匹配这样的同步节点，并执行相应点火变迁，直至到达标准特征约束模型的终止节点，同步匹配结束，此时表明该应用系统满足标准REST服务架构的特征约束；若在任一中间节点同步匹配失败，则说明该应用不满足标准REST架构的特征约束。查找基于REST服务架构应用系统的不符合标准特征之处，可以通过查找状态空间执行路径集合的差集来实现，即分析应用系统模型状态空间生成的路径中，与相应标准特征约束模型状态空间生成的路径相比，终止在哪个路径节点上，则该节点标识所反映的托肯(Token)信息，就能够提供直观的应用系统执行数据，即应用系统运行到这个状态时出现了不满足约束的执行状态数据，用于帮助系统设计者完成应用系统设计缺陷的定位及修正，使其满足标准REST服务架构约束。

4.2 验证方法的算法描述

上述验证方法中的核心，即状态空间中的执行路径同步匹配算法可描述如下：

假设：Nodes*={M0,M1,…,Mm},Arcs*={A0,A1,…,Am};/*一个标准特征约束模型状态空间的节点和路径集合*/

Nodes={N0,N1,…,Nn},Arcs={B0,B1,…,Bn};/*应用系统模型状态空间的节点和路径集合*/

AlgorithmSynchronizedPathMatch{

intm,n,i,j,k;/*便于描述状态空间中节点和路径的编号*/

While(i

if (Ni==M0andBi==A0){/*找到模型的初始同步节点*/

Find the initial synchronization node；

}

elsei++； }/*应用系统模型执行一次点火变迁，找到下一节点*/

j=i+1;//j指应用系统模型节点和路径编号

k=1;//k指标准特征约束模型节点和路径编号

While (j≤nandk≤m) {/*不能超出应用系统模型和标准特征约束模型的范围*/

在作业过程中出现异常应立即关闭发动机，检查出现异常的地方，堵塞的地方要及时清理，破损的地方及时更换，以免引起其他零部件发生破损。

if (Nj==MkandBj==Ak){/*依次查找两个模型的后继同步节点*/

Find the next synchronization node；

k++;j++;}/*应用系统模型和标准特征约束模型各执行一次点火变迁*/

else

while (j≤n) {/*在应用系统模型的节点和路径范围内*/

if (Nj==MkandBj==Ak) {/*继续查找后面的同步节点和点火变迁路径*/

Find the synchronization node;}

elsej++;}}/*应用系统模型执行一次点火变迁*/

if (k==m) return true；/*顺利匹配到终止同步节点，验证成功*/

else return false;/*未顺利匹配到终止同步状态，验证失败*/

}}

5 REST服务架构标准特征验证方法的实例应用

本节以基于REST服务架构的课程管理Web系统为例，验证上一节给出的验证方法的可用性和有效性，确认本文所提验证方法可以用于检验基于REST服务架构的Web应用系统设计是否符合REST服务架构的标准特征约束。

5.1 基于REST服务架构的Web应用系统建模

本节对一个自行研发的课程管理Web系统中的查询课程子功能进行CPN建模，构建得到的应用系统CPN模型关注查询课程进程中的资源交互和通信。如图7所示，对课程查询客户端、课程查询系统网关、课程查询系统服务器和课程查询系统数据库之间的通信行为进行了建模和分析，并使用基于模型状态空间执行路径同步匹配的验证方法确认该模型是否满足REST服务架构的五个标准特征约束。

Figure 7 CPN model of the course query subfunction图7 课程查询子功能的CPN模型

该模型中，由课程查询系统Web用户发出查询请求资源信息msg，该请求信息msg的数据定义为colsetMsg1=recordm:MSG*f:FORMAT*s:SENDER*r:RECEIVER，其中MSG、FORMAT、SENDER和RECEIVER均为字符串类型。通过通道ReqCHUG传送请求信息给课程查询系统的网关(Gateway)，然后由网关通过通道ReqCHGSC传送请求信息给课程查询系统服务器(Server)的缓存中。若该请求资源信息缓存在服务器的缓存SCache中(用ReqCHGSC变迁出弧表达式中的第一个元素分量m="1"来示例)，则服务器通过通道Reply1直接返回消息给该课程查询系统的用户；若该课程查询系统服务器的缓存中不存在该请求资源(用ReqCHGSC变迁出弧表达式中的第一个元素分量m="no"来示例)，则通过通道Search发送请求消息给该课程查询Web系统的数据库(Database)，然后从数据库中返回请求资源信息给系统用户。图8给出了课程查询子功能的CPN模型对应的状态空间。

Figure 8 State space of the course query subfunction model图8 课程查询子功能模型的状态空间

5.2 标准特征约束验证实例及分析

以图8给出的课程查询子功能CPN模型为基础，通过与3.2节的五个REST服务架构标准特征约束进行逐个比较，检验该课程查询子功能Web应用是否为标准的REST架构应用。(1)对客户端服务器标准特征约束进行检验，通过与3.2.1节的标准客户端服务器约束的状态空间执行路径进行比对，发现该REST架构模型不满足客户端服务器约束。由模型发现该应用模型的课程查询系统用户的功能等价于标准REST架构模型中的用户代理的功能， 该课程查询系统的网关功能等价于标准REST架构模型中的中间件，该课程查询系统的服务器功能等价于标准REST架构模型中源服务器的功能，该课程查询系统的数据库功能等价于标准REST架构模型中的资源的功能。经过使用同步路径匹配算法检验，图8中的节点1与图9中的节点1是初始同步节点，然后经过变迁路径发现该REST架构应用模型缺少其客户端的缓存功能，获取请求信息时要先看其缓存中是否存在，若不存在则继续向源服务器请求资源信息，故该课程查询子功能Web系统应增加客户端的缓存功能。

Figure 9 State space of standard client server constraints图9 标准客户端服务器约束状态空间图

Figure 10 State space of standard cachable constraints图10 标准可缓存约束状态空间图

(2)对可缓存标准特征约束进行检验，通过与3.2.2节的标准可缓存约束模型的状态空间执行路径进行比对，发现该REST架构模型不满足可缓存约束。经过使用同步路径匹配算法检验，可发现图8中的节点1与图10中的节点1是初始同步节点，从后继变迁路径中可发现该课程查询系统的用户端和网关均缺少缓存功能，故该课程查询子功能Web系统应增加相应的缓存机制。

Figure 11 Corrected CPN model of the course query subfunction图11 课程查询子功能的修正CPN模型

(3)对分层标准特征约束进行检验，通过对其状态空间执行路径验证，发现该REST架构模型满足分层约束。通过与3.2.4节的标准分层约束的状态空间执行路径进行比对，该课程查询系统用户只能通过课程查询系统的网关进行交互，课程查询系统的数据库只能和服务器进行通信，该课程查询子功能Web系统满足分层标准特征约束。同时,对无状态和统一接口标准特征约束进行检验，通过3.2.3节的标准无状态约束的状态空间执行路径比对，可以发现该REST架构的课程查询系统满足无状态约束，消息的所有信息可包含在发送的请求和回答信息中，主要内容存储在服务器中，服务器是无状态的；通过与3.2.5节的标准统一接口约束的状态空间执行路径比对，发现该模型满足统一接口约束，请求和响应的消息格式是一致的，都是msg形式，当两次发送的请求信息相同时，响应信息是相同的，故满足统一接口约束。

通过以上的分析，图11给出了修改后的基于REST服务架构的课程查询子功能应用系统的CPN模型，经再次使用本文所提方法确认，该应用系统满足了REST服务架构的各项标准特征约束。从图7和图11的对比分析可看出：(1)图11比图7增加了Users Cache缓存功能，其可以为课程管理Web系统的客户端增加缓存功能；(2)图11比图7增加了Gateway Cache缓存功能，其可以为课程管理Web系统的网关增加缓存功能。增加以上两个缓存器，使得系统功能更加完善，当课程管理Web系统的客户端发出请求信息时，首先检验其内部缓存中是否存在该资源，如果其缓存中存在该资源(用ReqCHUC变迁出弧表达式中的第四个元素分量r="4"来示例)，则直接返回响应消息给客户端；若不存在客户端缓存中(用ReqCHUC变迁出弧表达式中的第四个元素分量r="Ucache"来示例)，需要向课程管理Web系统的网关请求资源，若该资源存在网关的缓存中(用ReqCHUG变迁出弧表达式中的第四个元素分量r="Ucache"来示例)，则直接返回响应消息给客户端。

6 结束语

实现基于REST服务架构的Web系统前，验证该系统设计是否满足REST服务架构标准特征是至关重要的，能够有效提升基于REST服务架构的Web系统的研发质量。本文提出了一种基于CPN模型的REST服务架构标准特征验证方法。首先，给出了REST服务架构的五个标准特征约束的CPN模型描述，以此为基础，提出了一种基于模型状态空间执行路径同步匹配的验证方法，以应用系统的CPN模型和标准特征约束的CPN模型为基础，对模型状态空间中的各自执行路径进行同步匹配，若路径可同步执行完毕则说明该应用系统满足该REST标准特征约束。最后，以基于REST服务架构的课程查询功能系统为实际应用，确认了上述验证方法的可用性，应用本文所提验证方法可以有效确认基于REST服务架构的Web应用系统设计是否符合REST服务架构的标准特征约束，并在不符合标准特征约束时提供直观、可行的执行数据，便于后续完成应用系统设计缺陷定位及修正。下一步工作需强化验证方法核心过程的形式描述和有效性确认，并以更多基于REST服务架构的典型应用系统为实践对象应用本方法，完善方法执行细节，提升方法的可用性。

[1] Fielding R T. Architectural styles and the design of network-based software architectures [D]. Irvine:University of California, 2000.

[2] Paganelli F,Turchi S,Giuli D.A web of things framework for RESTful applications and its experimentation in a smart city[J].IEEE Systems Journal,2016,10(4):1412-1423.

[3] Song Yi-shan,Xu Ke,Liu Ke.Research on web instant messaging using REST web service[C]∥Proc of 2010 IEEE the 2nd Symposium on Web Society,2010:497-500.

[4] Liu Jing,Ye Xin-ming,Zhou Jian-tao.Colored Petri net hierarchical model of complex network software and model integration verification method[J].High-tech Communications,2013,23(11):1139-1147.(in Chinese)

[5] Benabdelhafid M S,Boufaida M.Toward a better interoperability of enterprise information systems:A CPNs and timed CPNs-based web service interoperability verification in a choreography[J].Procedia Technology,2014,16:269-278.

[6] Sun Lian-xia.Dynamic composition modeling and validation of web services based on hierarchical colored Petri nets[D].Dongying:China University of Petroleum,2011.(in Chinese)

[7] Costa B, Pires P F, Delicato F C, et al.Evaluating REST architectures—Approach,tooling and guidelines[J].The Journal of Systems and Software,2016,112:156-180.

[8] Jensen K,Kristence L M,Weels L.Coloured Petri nets and CPN tools for modeling and validation of concurrent systems[J].International Journal on Software Tools for Technology Transfer,2007,9(3-4):213-254.

[9] Jensen K,Kristence L M.Coloured Petri nets:Modelling and validation of concurrent systems[J].Berlin:Springer,2009:95-188.

[10] Wu Xi, Zhu Hui-biao.Formalization and analysis of the REST architecture from the process algebra perspective[J].Future Generation Computer Systems,2016,56:153-168.

[11] Yuan Ting.Formal modeling and analysis of RESTful web services[D].Shanghai:East China Normal University,2015.(in Chinese)

[12] Adhipta D,Hassan M F,Mahmood A K.Web services extension model simulation in hierarchical colored Petri net[C]∥Proc of International Conference on Computer & Information Science,2012:741-746.

附中文参考文献：

[4] 刘靖,叶新铭,周建涛.复杂网络软件的着色Petri网层次建模及模型集成确认方法[J].高技术通讯,2013,23(11):1139-1147.

[6] 孙连侠,基于分层着色Petri网的Web服务动态组合建模与验证[D].东营：中国石油大学,2011.

[11] 袁婷.RESTful Web服务的形式化建模与分析[J].上海：华东师范大学,2015.