趙玉強(qiáng),劉 靖

(內(nèi)蒙古大學(xué)計算機(jī)學(xué)院，內(nèi)蒙古 呼和浩特 010021)

1 引言

2000年,Fielding[1]在其博士學(xué)位論文中首先提出REST(REpresentational State Transfer)服務(wù)架構(gòu)，是指一種結(jié)合超文本傳輸協(xié)議HTTP(Hyper Text Transfer Protocol)標(biāo)準(zhǔn)和統(tǒng)一資源標(biāo)識符URI(Uniform Resource Identifier)標(biāo)準(zhǔn)的設(shè)計原理抽象成的新風(fēng)格，其面向資源并強(qiáng)調(diào)以資源為中心。當(dāng)前REST服務(wù)架構(gòu)在企業(yè)中應(yīng)用越來越廣泛，很多Web應(yīng)用系統(tǒng)都是基于REST服務(wù)架構(gòu)研發(fā)的，例如Amazon購物網(wǎng)站和Google搜索引擎等[2]。REST服務(wù)架構(gòu)的優(yōu)點(diǎn)包括：瀏覽器作為客戶端，這樣可以簡化軟件需求；利用緩存機(jī)制提高訪問速度；通信的無狀態(tài)性可以讓不同服務(wù)器處理一系列請求中的不同請求，提高服務(wù)器可擴(kuò)展性；降低Web系統(tǒng)開發(fā)的復(fù)雜性，提高系統(tǒng)的可擴(kuò)展性等。

當(dāng)前也有一些應(yīng)用REST服務(wù)架構(gòu)的Web應(yīng)用系統(tǒng)不遵循REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征約束，故帶來相應(yīng)的諸多問題。比如，不滿足無狀態(tài)約束會破壞系統(tǒng)的可伸縮性，會影響系統(tǒng)負(fù)載均衡；不滿足客戶端服務(wù)器約束會增加系統(tǒng)服務(wù)器的開銷，增加響應(yīng)時間；不滿足可緩存約束會帶來更多的時間開銷，因?yàn)槊看握{(diào)取資源都需向服務(wù)器請求，故會增加時間開銷等[3]。因此，為防止以上問題的出現(xiàn)，在設(shè)計基于REST服務(wù)架構(gòu)的Web應(yīng)用系統(tǒng)時，需要對該系統(tǒng)設(shè)計是否滿足REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征進(jìn)行驗(yàn)證，以提升基于REST服務(wù)架構(gòu)的Web系統(tǒng)的研發(fā)質(zhì)量。

目前針對REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征驗(yàn)證的形式化驗(yàn)證方法，主要包括基于有限狀態(tài)機(jī)和CSP (Communicating Sequential Processes)等方法。在基于有限狀態(tài)機(jī)模型的驗(yàn)證中，不支持分層和緩存確認(rèn)，而使用CSP方法抽象程度較高，描述更加復(fù)雜。因此，鑒于CPN(Colored Petri Nets)模型在可視化和層次化建模、復(fù)雜數(shù)據(jù)描述、并發(fā)行為描述和動態(tài)執(zhí)行等方面的優(yōu)勢和廣泛應(yīng)用[4 - 6]，本文提出一種基于CPN模型的REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征驗(yàn)證方法，首先，對REST服務(wù)架構(gòu)的標(biāo)準(zhǔn)特征約束進(jìn)行CPN建模，包括客戶端-服務(wù)器約束(Client-Server Constraint)、可緩存約束(Cacheable Constraint)、無狀態(tài)約束(Stateless Constraint)、分層約束(Layered Constraint)、統(tǒng)一接口約束(Uniform Interface Constraint)等；其次，實(shí)現(xiàn)基于模型狀態(tài)空間執(zhí)行路徑同步匹配的驗(yàn)證，即以應(yīng)用系統(tǒng)的CPN模型和標(biāo)準(zhǔn)特征約束的CPN模型為基礎(chǔ)，對模型狀態(tài)空間中的各自執(zhí)行路徑進(jìn)行同步匹配，若路徑可同步執(zhí)行完畢，則說明該應(yīng)用系統(tǒng)滿足該REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征約束。文中以自行研發(fā)的基于REST服務(wù)架構(gòu)的課程管理Web系統(tǒng)為例，驗(yàn)證上述驗(yàn)證方法的可用性和有效性，實(shí)驗(yàn)結(jié)果表明，本文所提驗(yàn)證方法可以有效確認(rèn)基于REST服務(wù)架構(gòu)的Web應(yīng)用系統(tǒng)設(shè)計是否符合REST服務(wù)架構(gòu)的標(biāo)準(zhǔn)特征約束，并在不符合標(biāo)準(zhǔn)特征約束時提供直觀、可行的執(zhí)行數(shù)據(jù)，便于后續(xù)完成應(yīng)用系統(tǒng)設(shè)計缺陷定位及修正。

2 相關(guān)工作基礎(chǔ)

2.1 REST服務(wù)架構(gòu)的基本概念

REST架構(gòu)以資源為中心，資源是REST架構(gòu)中最關(guān)鍵的抽象概念，任何單元都可以成為資源。同時所有資源要有統(tǒng)一的資源標(biāo)識符，使用URI作為資源標(biāo)識符，對資源的操作不會改變資源標(biāo)識符，并且所有的操作是無狀態(tài)的。RESTful Web服務(wù)主要使用HTTP協(xié)議中的四種方法，包含POST、GET、PUT和DELETE方法。其中，POST方法是新增數(shù)據(jù)，即新增一個沒有ID的資源；GET方法是對數(shù)據(jù)進(jìn)行讀取，獲取一個已有資源；PUT方法是對數(shù)據(jù)進(jìn)行更新，更新一個資源或新增一個沒有含ID的資源，用給定的表述信息替換資源的當(dāng)前狀態(tài)；DELETE方法是刪除一個資源，并且刪除請求有一個重要的屬性，它是冪等的。所謂冪等，就是發(fā)送多次請求對資源狀態(tài)的影響和發(fā)送一次請求的影響是一樣的[7]。

REST架構(gòu)主要元素包含數(shù)據(jù)單元、連接器和組件。其中，數(shù)據(jù)單元主要由資源、資源標(biāo)識符、表示符、表示元數(shù)據(jù)、資源元數(shù)據(jù)和控制數(shù)據(jù)組成。連接器作為統(tǒng)一接口用于各組件相互通信和訪問資源，主要由客戶端、服務(wù)器、緩存、解析器和通道組成，連接器封裝了資源的底層實(shí)現(xiàn)和溝通機(jī)制。組件主要包括用戶代理、源服務(wù)器和中間件，根據(jù)他們在應(yīng)用程序中發(fā)揮的作用劃分角色。

2.2 CPN方法概述

本文使用CPN技術(shù)對REST服務(wù)架構(gòu)進(jìn)行建模，實(shí)驗(yàn)工具為CPN Tools，可以有效支持模型的驗(yàn)證分析。CPN是一種形式化建模方法，由傳統(tǒng)的Petri網(wǎng)演變而來，是一種高級Petri網(wǎng)。同時CPN具有很強(qiáng)的數(shù)學(xué)建模能力，與數(shù)學(xué)密切相關(guān)，常用于對復(fù)雜、并發(fā)系統(tǒng)的建模分析。CPN建模語言具有一個兼具語法和語義的數(shù)學(xué)定義。驗(yàn)證方法涉及數(shù)學(xué)公式屬性和計算機(jī)輔助證明，該屬性由模型實(shí)現(xiàn)。

本文使用的CPN檢驗(yàn)方法包含如下兩種：模擬(Simulation)執(zhí)行檢驗(yàn)方法和狀態(tài)空間(State Space)檢驗(yàn)方法。模擬執(zhí)行檢驗(yàn)方法通過對應(yīng)用系統(tǒng)建模，驗(yàn)證系統(tǒng)每一步的狀態(tài)變遷，檢驗(yàn)系統(tǒng)模型是否滿足預(yù)期[8]。狀態(tài)空間檢驗(yàn)方法通過對系統(tǒng)模擬執(zhí)行后生成相應(yīng)的狀態(tài)空間，該狀態(tài)空間即系統(tǒng)的可執(zhí)行路徑，即CPN模型的所有可達(dá)狀態(tài)和狀態(tài)變化情況，并將其通過有向圖表示出來，其中，節(jié)點(diǎn)表示狀態(tài)，弧代表發(fā)生的事件，狀態(tài)空間可以自動生成。本文使用CPN方法對REST服務(wù)架構(gòu)應(yīng)用建模，通過狀態(tài)的變遷模擬應(yīng)用服務(wù)的資源變化，可有效對其進(jìn)行驗(yàn)證。

CPN使用九元組CPN=(P,T,A,∑,V,C,G,E,I)[9]來表示，各元素定義如表1所示。本文使用的CPN方法嚴(yán)格按照標(biāo)準(zhǔn)來定義。

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

2.3 相關(guān)工作

文獻(xiàn)[7]提出了一種評估REST架構(gòu)的方法、工具和指導(dǎo)法則，并在ATAM(Architecture Trade off Analysis Method)場景下對該方法進(jìn)行評估，綜合考慮多種屬性，驗(yàn)證該方法的正確性。

文獻(xiàn)[10]主要使用CSP方法對REST架構(gòu)進(jìn)行形式化建模，該方法首先對資源的調(diào)用過程進(jìn)行分析，抽象出四個主要進(jìn)程組件，包含用戶代理(User Agent)、中間件(Intermediary)、源服務(wù)器(Origin Server)和資源(Resource)，并表示出四個進(jìn)程的通信。其次，對基于程分析工具包PAT(Process Analysis Toolkit)模型檢驗(yàn)工具和時序邏輯描述對REST服務(wù)架構(gòu)的標(biāo)準(zhǔn)特征約束進(jìn)行分析和驗(yàn)證。文獻(xiàn)[11]同樣使用CSP方法對RESTful Web服務(wù)進(jìn)行建模與分析，將REST架構(gòu)模型抽象成客戶端、服務(wù)器和資源三個模塊，用CSP描述REST架構(gòu)中的進(jìn)程及其具體方法行為，使用一階邏輯對Web服務(wù)的無狀態(tài)等屬性進(jìn)行描述，并基于PAT工具進(jìn)行驗(yàn)證。此外，文獻(xiàn)[12]使用層次CPN對Web Services系統(tǒng)模型進(jìn)行行為模擬，并基于生成的狀態(tài)空間完成功能驗(yàn)證，主要是證明Web Services擴(kuò)展模型可以提高信息的通信傳輸性能。通過以上研究可知，使用CPN模型對Web應(yīng)用系統(tǒng)進(jìn)行建模、分析和驗(yàn)證是可行的。

綜上，目前對REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征的驗(yàn)證研究工作主要集中在基于CSP的方法上，但這類驗(yàn)證方法抽象程度較高，描述較為復(fù)雜。本文充分利用CPN建模技術(shù)的優(yōu)勢，提出一種基于CPN模型的REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征驗(yàn)證方法，可以有效確認(rèn)基于REST服務(wù)架構(gòu)的Web應(yīng)用系統(tǒng)設(shè)計是否符合REST服務(wù)架構(gòu)的標(biāo)準(zhǔn)特征約束，并在不符合標(biāo)準(zhǔn)特征約束時提供直觀、可行的執(zhí)行數(shù)據(jù)，便于后續(xù)完成應(yīng)用系統(tǒng)設(shè)計缺陷定位及修正。

3 REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征的CPN建模

3.1 REST服務(wù)架構(gòu)的進(jìn)程視圖

由于REST服務(wù)架構(gòu)很強(qiáng)調(diào)資源的調(diào)用過程，一切以資源為中心，故REST服務(wù)架構(gòu)的進(jìn)程視圖用來對REST架構(gòu)資源交互進(jìn)行描述，表示出不同組件之間的交互關(guān)系。參考文獻(xiàn)[8]的描述，圖1給出了REST服務(wù)架構(gòu)進(jìn)程視圖中四個主要組件的交互示例。

Figure 1 Four main parts of the REST service architecture application model圖1 REST服務(wù)架構(gòu)應(yīng)用模型的四個主要部分

REST服務(wù)架構(gòu)的進(jìn)程視圖主要包含用戶代理、中間件、源服務(wù)器和資源四個組件，組件之間的交互通過通道和接口進(jìn)行，且都有統(tǒng)一接口，用戶代理、中間件和源服務(wù)器有內(nèi)部緩存機(jī)制[8]，相互間的通道在圖中描述為CHIOS、CHOSR和CHUAI等，實(shí)現(xiàn)基于通道機(jī)制的信息發(fā)送與接收。

具體而言，用戶代理(即客戶端)發(fā)送請求消息時，首先請求其內(nèi)部緩存以得到資源，若存在其內(nèi)部緩存中則直接返回給用戶代理。若其內(nèi)部緩存不存在該資源，那么就需向外部網(wǎng)絡(luò)中間件發(fā)送請求消息。這里定義兩者之間的內(nèi)部通道為CHUAI。請求消息可以描述為四元組(GET,PUT,POST,DELETE)，所有消息都以同樣的四元組形式表示，該四元組內(nèi)元素的具體含義參見2.1節(jié)描述。中間件主要由代理(Proxy)或網(wǎng)關(guān)(Gateway)組成，也有緩存功能。中間件的主要目的是轉(zhuǎn)發(fā)消息和傳輸信息。用戶代理向中間件發(fā)送請求信息，中間件有兩種方式查詢資源，一種是向其內(nèi)部緩存Cache請求資源，另一種是向源服務(wù)器請求資源，這里通過內(nèi)部通道CHIOS進(jìn)行通信。用戶代理需要的資源都存儲在源服務(wù)器上，源服務(wù)器是唯一可以與資源通信的組件。用戶代理可以通過中間件與源服務(wù)器進(jìn)行通信，源服務(wù)器收到請求資源信息后，先檢查其緩存，如果其緩存沒有該資源，則源服務(wù)器將請求信息發(fā)送給資源，并將請求資源返回給中間件。源服務(wù)器與資源之間的通信通過CHOSR通道進(jìn)行。

3.2 基于CPN模型的REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征約束建模

3.2.1 客戶端-服務(wù)器約束

用戶代理和源服務(wù)器作為兩個獨(dú)立的組件，通過統(tǒng)一接口將它們分離。客戶端服務(wù)器約束對REST架構(gòu)應(yīng)用C/S架構(gòu)特征進(jìn)行規(guī)范，即REST是一種典型的 C/S架構(gòu)，該約束保證通信只能由客戶端單方面發(fā)起，表現(xiàn)為請求-響應(yīng)的形式。REST架構(gòu)強(qiáng)調(diào)瘦服務(wù)器端，服務(wù)器端只處理跟資源相關(guān)的操作，所有顯示工作都應(yīng)該在客戶端。用戶代理向其內(nèi)部緩存或源服務(wù)器發(fā)送請求資源信息，忽略資源不存在的情況，用戶代理請求的信息必須存在于其內(nèi)部緩存或源服務(wù)器中，用戶代理發(fā)出的所有請求消息，都會得到其緩存或源服務(wù)器的回復(fù)。

圖2給出了REST服務(wù)架構(gòu)中客戶端服務(wù)器標(biāo)準(zhǔn)特征約束的CPN模型。首先，用戶代理即客戶端發(fā)出請求資源信息msg，msg描述為Msg1類型的變量，該類型在CPN建模中描述為record預(yù)定義類型：colsetMsg1=recordm:MSG*f:FORMAT*s:SENDER*r:RECEIVER，其中四個元素均為String字符串類型，MSG描述請求資源的內(nèi)容，F(xiàn)ORMAT描述請求資源的格式，SENDER描述請求消息發(fā)出者，RECEIVER描述響應(yīng)消息的發(fā)出者。其次，查詢用戶代理的緩存中是否存在該資源信息，若該資源在其緩存中(用通道請求RequestUserAgent-Cache簡稱RequestUC變遷出弧表達(dá)式中的第一個元素分量m="1"來示例)，則由其緩存返回響應(yīng)信息給用戶代理；若其緩存中不存在該請求資源(用RequestUC變遷出弧表達(dá)式中的第一個元素分量m="no"來示例)，則需要去源服務(wù)器中再次請求資源。最后，把客戶端請求的資源信息返回給用戶代理。

Figure 2 CPN model of client-server constraints圖2 客戶端-服務(wù)器約束的CPN模型

3.2.2 可緩存約束

用戶代理、中間件和源服務(wù)器均具有緩存機(jī)制，請求資源信息可以被保存在相應(yīng)的內(nèi)部緩存器中，可改善無狀態(tài)特性帶來的低效性?？删彺婕s束用來檢驗(yàn)用戶代理、中間件和源服務(wù)器是否均具有緩存功能，響應(yīng)信息可保留在這三個內(nèi)部緩存中，可緩存屬性有效提高了訪問性能，縮短系統(tǒng)響應(yīng)時間，為用戶代理帶來便利。本文只考慮可緩存的請求信息。如果用戶代理首次發(fā)送請求信息，則緩存中不存在任何信息，故應(yīng)向源服務(wù)器請求資源信息。否則，用戶代理可能直接從其內(nèi)部緩存中獲得資源，無需訪問服務(wù)器。如果兩個請求資源信息功能相同，則第二個可直接訪問緩存獲得資源信息。

Figure 3 CPN model of cachable constraints圖3 可緩存約束的CPN模型

圖3給出了REST服務(wù)架構(gòu)的可緩存標(biāo)準(zhǔn)特征約束模型。首先，用戶代理發(fā)出請求資源信息，該請求資源信息msg描述同上節(jié)。其次，查詢用戶代理的緩存中是否存在該資源信息，若資源存在其內(nèi)部緩存中(用通道請求RequestUserAgent-Cache,簡稱RequestUC變遷出弧表達(dá)式中的第一個元素分量m="1"來示例)，則由其內(nèi)部緩存直接返回信息給用戶代理；若用戶代理的內(nèi)部緩存中不存在該請求資源(用RequestUC變遷出弧表達(dá)式中的第一個元素分量m="no"來示例)，則需要向網(wǎng)絡(luò)中間件(Intermediary)繼續(xù)發(fā)送請求信息，若存在其緩存中(用通道請求RequestUserAgent-IntermediaryCache,簡稱RequestUIC變遷出弧表達(dá)式中的第四個元素分量r="Ucache"來示例)，就把資源信息返回給用戶代理；若中間件緩存中不存在該請求資源信息(用RequestUIC變遷出弧表達(dá)式中的第四個元素分量r="Icache"來示例)，則需要向源服務(wù)器發(fā)送請求信息，若源服務(wù)器緩存存在該資源信息(用通道請求RequestUserAgent-ServerCache，簡稱RequestSC變遷入弧表達(dá)式中的第四個元素分量r="Icache"來示例)，則返回給用戶代理。最后，若源服務(wù)器緩存中不存在該資源信息(用RequestSC變遷入弧表達(dá)式中的第四個元素分量r="Scache"來示例)，需要向數(shù)據(jù)源請求信息，最終返回響應(yīng)消息給用戶代理。

3.2.3 無狀態(tài)約束

REST服務(wù)架構(gòu)中的服務(wù)器端不保存任何與客戶端的會話狀態(tài)信息。所有狀態(tài)信息只存在通信消息中，即用戶代理發(fā)送到服務(wù)器的請求消息必須包含理解該消息的所有信息。無狀態(tài)指會話狀態(tài)信息保留在用戶代理中，服務(wù)器是無狀態(tài)的，如果請求信息同時來自不同的用戶代理時，但多個用戶代理的請求資源信息相同，則源服務(wù)器將反饋給用戶代理相同的資源信息。REST服務(wù)架構(gòu)的狀態(tài)指客戶端的狀態(tài)，每個資源在客戶端的表述就是客戶端的一個狀態(tài)。狀態(tài)信息可描述為三元組(id，data，oper)形式，id是指資源標(biāo)識符的id，data是指資源信息內(nèi)容，oper是指具體的操作，即GET、PUT、POST和DELETE等操作。

圖4給出了REST架構(gòu)的無狀態(tài)標(biāo)準(zhǔn)特征約束模型。首先，兩個用戶代理之間的通信內(nèi)容都包含在請求信息中，并且用戶代理只保存兩者的通信內(nèi)容。其次，用戶代理通過通道Request向源服務(wù)器發(fā)送請求資源信息，然后返回給用戶代理。若多個用戶代理請求的資源信息相同時，得到的響應(yīng)信息也必須是一致的(兩個用戶代理得到的響應(yīng)信息均為{m="1",f="2",s="3",r="4"})，則表明該REST架構(gòu)的服務(wù)器是無狀態(tài)的。

Figure 4 CPN model of stateless constraints圖4 無狀態(tài)約束的CPN模型

3.2.4 分層約束

分層約束檢驗(yàn)REST服務(wù)架構(gòu)Web應(yīng)用是否符合三層架構(gòu)特性，分層約束提高了各層之間的獨(dú)立性和系統(tǒng)的可伸縮性。在REST服務(wù)架構(gòu)Web應(yīng)用系統(tǒng)中，組件只能和其鄰接組件通信，即用戶代理若想發(fā)送請求信息時，只能發(fā)送給其內(nèi)部緩存或者中間件，不能直接發(fā)送給源服務(wù)器，同樣源服務(wù)器也不能直接返回響應(yīng)消息給用戶代理，該約束將REST架構(gòu)分解為若干等級的層，其他組件之間的通信也相同。在分層約束條件中，REST架構(gòu)只考慮三層REST應(yīng)用系統(tǒng)，即用戶代理層、中間件層和服務(wù)器層。

圖5給出了REST架構(gòu)的分層標(biāo)準(zhǔn)特征約束模型。

Figure 5 CPN model of layered constraints圖5 分層約束的CPN模型

首先，該REST架構(gòu)是標(biāo)準(zhǔn)的三層架構(gòu)應(yīng)用。其次，用戶代理只能向中間件發(fā)出請求資源信息(用戶代理和中間件兩者的交互通過通道CHUAI進(jìn)行)，然后中間件繼續(xù)向源服務(wù)器發(fā)送請求信息(中間件和源服務(wù)器兩者的交互通過通道CHIOS進(jìn)行)，最后把請求的資源信息再逐步通過以上的接口返回給用戶代理。其中，由通道CHUAI和通道CHIOS將三個組件分為三層模型。

3.2.5 統(tǒng)一接口約束

統(tǒng)一接口約束檢驗(yàn)組件間通信消息格式是否一致，即檢驗(yàn)REST架構(gòu)應(yīng)用的接口是否一致，該約束可改善系統(tǒng)的交互性和可重用性。在該約束條件中，體現(xiàn)在用戶代理發(fā)送的請求消息和源服務(wù)器返回的消息格式必須是一致的，即資源的標(biāo)識符是一致的。請求消息描述為四元組表示{msg,r_format,sender,receiver}，其中,msg表示請求的資源，r_format表示資源的格式，sender表示資源的請求發(fā)送者，receiver表示資源的請求接收者。

圖6給出了REST架構(gòu)的統(tǒng)一接口標(biāo)準(zhǔn)特征約束模型。表明用戶代理向源服務(wù)器發(fā)送的請求信息和服務(wù)器的響應(yīng)信息格式是一致的(用Reply變遷出弧表達(dá)式中的第一個元素分量m="1"來示例)，發(fā)送者和接收者的信息應(yīng)該具有相同的資源標(biāo)識符，這體現(xiàn)出REST架構(gòu)的統(tǒng)一接口標(biāo)準(zhǔn)特性。

Figure 6 CPN model of uniform interface constraints圖6 統(tǒng)一接口約束的CPN模型

4 REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征驗(yàn)證方法

本節(jié)提出一種基于CPN模型的REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征驗(yàn)證方法，以應(yīng)用系統(tǒng)的CPN模型和標(biāo)準(zhǔn)特征約束的CPN模型為基礎(chǔ)，對模型狀態(tài)空間中的各自執(zhí)行路徑進(jìn)行同步匹配，若路徑可同步執(zhí)行則說明該應(yīng)用系統(tǒng)滿足該REST標(biāo)準(zhǔn)特征約束。若不符合標(biāo)準(zhǔn)特征約束時，提供直觀、可行的執(zhí)行數(shù)據(jù)，便于后續(xù)完成應(yīng)用系統(tǒng)設(shè)計缺陷定位及修正。

4.1 驗(yàn)證方法的基本思想

本文所提驗(yàn)證方法的核心思想可概述為：構(gòu)建應(yīng)用系統(tǒng)的CPN模型和標(biāo)準(zhǔn)特征約束的CPN模型，分別生成各自的狀態(tài)空間，得到各模型相應(yīng)的執(zhí)行路徑集合。執(zhí)行基于模型狀態(tài)空間的同步路徑匹配算法，逐個檢驗(yàn)應(yīng)用系統(tǒng)模型的狀態(tài)空間執(zhí)行路徑是否同步包含標(biāo)準(zhǔn)特征約束模型的路徑，若包含，則驗(yàn)證成功；否則存在不符合之處，通過狀態(tài)差集定位應(yīng)用系統(tǒng)模型及系統(tǒng)設(shè)計中的缺陷錯誤，找出不符合的狀態(tài)和路徑，對其進(jìn)行修改完善，使其滿足REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征約束。

具體而言，執(zhí)行基于模型狀態(tài)空間的同步路徑匹配算法是核心。首先，我們給出一個核心概念，即同步節(jié)點(diǎn)。若REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征約束模型狀態(tài)空間的一個節(jié)點(diǎn)使用M*來標(biāo)識，應(yīng)用系統(tǒng)模型狀態(tài)空間的一個節(jié)點(diǎn)使用M標(biāo)識，如果M*的Marking值和M的功能等價，即兩個節(jié)點(diǎn)標(biāo)記中的關(guān)鍵字段數(shù)據(jù)相同，并且后續(xù)可執(zhí)行變遷描述的功能也相同，則這兩個節(jié)點(diǎn)可互稱為同步節(jié)點(diǎn)。狀態(tài)空間執(zhí)行路徑的同步包含是指同步節(jié)點(diǎn)和變遷路徑的包含關(guān)系，并且同步節(jié)點(diǎn)和變遷路徑的執(zhí)行順序也要一致有序。算法的關(guān)鍵部分就是其中的狀態(tài)空間執(zhí)行路徑完成同步執(zhí)行匹配，直觀而言，從狀態(tài)空間執(zhí)行路徑生成的角度分析，由應(yīng)用系統(tǒng)模型的初始狀態(tài)開始執(zhí)行可能的點(diǎn)火變遷，在經(jīng)過一個或多個變遷點(diǎn)火后，得到與標(biāo)準(zhǔn)特征約束模型起始節(jié)點(diǎn)可同時執(zhí)行的同步節(jié)點(diǎn)；然后，點(diǎn)火同步節(jié)點(diǎn)，執(zhí)行一步操作后，應(yīng)用系統(tǒng)模型又可能經(jīng)過一個或多個變遷點(diǎn)火，再次得到與標(biāo)準(zhǔn)特征約束模型起始節(jié)點(diǎn)可同時執(zhí)行的下一個同步節(jié)點(diǎn)；依次匹配這樣的同步節(jié)點(diǎn)，并執(zhí)行相應(yīng)點(diǎn)火變遷，直至到達(dá)標(biāo)準(zhǔn)特征約束模型的終止節(jié)點(diǎn)，同步匹配結(jié)束，此時表明該應(yīng)用系統(tǒng)滿足標(biāo)準(zhǔn)REST服務(wù)架構(gòu)的特征約束；若在任一中間節(jié)點(diǎn)同步匹配失敗，則說明該應(yīng)用不滿足標(biāo)準(zhǔn)REST架構(gòu)的特征約束。查找基于REST服務(wù)架構(gòu)應(yīng)用系統(tǒng)的不符合標(biāo)準(zhǔn)特征之處，可以通過查找狀態(tài)空間執(zhí)行路徑集合的差集來實(shí)現(xiàn)，即分析應(yīng)用系統(tǒng)模型狀態(tài)空間生成的路徑中，與相應(yīng)標(biāo)準(zhǔn)特征約束模型狀態(tài)空間生成的路徑相比，終止在哪個路徑節(jié)點(diǎn)上，則該節(jié)點(diǎn)標(biāo)識所反映的托肯(Token)信息，就能夠提供直觀的應(yīng)用系統(tǒng)執(zhí)行數(shù)據(jù)，即應(yīng)用系統(tǒng)運(yùn)行到這個狀態(tài)時出現(xiàn)了不滿足約束的執(zhí)行狀態(tài)數(shù)據(jù)，用于幫助系統(tǒng)設(shè)計者完成應(yīng)用系統(tǒng)設(shè)計缺陷的定位及修正，使其滿足標(biāo)準(zhǔn)REST服務(wù)架構(gòu)約束。

4.2 驗(yàn)證方法的算法描述

上述驗(yàn)證方法中的核心，即狀態(tài)空間中的執(zhí)行路徑同步匹配算法可描述如下：

假設(shè)：Nodes*={M0,M1,…,Mm},Arcs*={A0,A1,…,Am};/*一個標(biāo)準(zhǔn)特征約束模型狀態(tài)空間的節(jié)點(diǎn)和路徑集合*/

Nodes={N0,N1,…,Nn},Arcs={B0,B1,…,Bn};/*應(yīng)用系統(tǒng)模型狀態(tài)空間的節(jié)點(diǎn)和路徑集合*/

AlgorithmSynchronizedPathMatch{

intm,n,i,j,k;/*便于描述狀態(tài)空間中節(jié)點(diǎn)和路徑的編號*/

While(i

if (Ni==M0andBi==A0){/*找到模型的初始同步節(jié)點(diǎn)*/

Find the initial synchronization node；

}

elsei++； }/*應(yīng)用系統(tǒng)模型執(zhí)行一次點(diǎn)火變遷，找到下一節(jié)點(diǎn)*/

j=i+1;//j指應(yīng)用系統(tǒng)模型節(jié)點(diǎn)和路徑編號

k=1;//k指標(biāo)準(zhǔn)特征約束模型節(jié)點(diǎn)和路徑編號

While (j≤nandk≤m) {/*不能超出應(yīng)用系統(tǒng)模型和標(biāo)準(zhǔn)特征約束模型的范圍*/

在作業(yè)過程中出現(xiàn)異常應(yīng)立即關(guān)閉發(fā)動機(jī)，檢查出現(xiàn)異常的地方，堵塞的地方要及時清理，破損的地方及時更換，以免引起其他零部件發(fā)生破損。

if (Nj==MkandBj==Ak){/*依次查找兩個模型的后繼同步節(jié)點(diǎn)*/

Find the next synchronization node；

k++;j++;}/*應(yīng)用系統(tǒng)模型和標(biāo)準(zhǔn)特征約束模型各執(zhí)行一次點(diǎn)火變遷*/

else

while (j≤n) {/*在應(yīng)用系統(tǒng)模型的節(jié)點(diǎn)和路徑范圍內(nèi)*/

if (Nj==MkandBj==Ak) {/*繼續(xù)查找后面的同步節(jié)點(diǎn)和點(diǎn)火變遷路徑*/

Find the synchronization node;}

elsej++;}}/*應(yīng)用系統(tǒng)模型執(zhí)行一次點(diǎn)火變遷*/

if (k==m) return true；/*順利匹配到終止同步節(jié)點(diǎn)，驗(yàn)證成功*/

else return false;/*未順利匹配到終止同步狀態(tài)，驗(yàn)證失敗*/

}}

5 REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征驗(yàn)證方法的實(shí)例應(yīng)用

本節(jié)以基于REST服務(wù)架構(gòu)的課程管理Web系統(tǒng)為例，驗(yàn)證上一節(jié)給出的驗(yàn)證方法的可用性和有效性，確認(rèn)本文所提驗(yàn)證方法可以用于檢驗(yàn)基于REST服務(wù)架構(gòu)的Web應(yīng)用系統(tǒng)設(shè)計是否符合REST服務(wù)架構(gòu)的標(biāo)準(zhǔn)特征約束。

5.1 基于REST服務(wù)架構(gòu)的Web應(yīng)用系統(tǒng)建模

本節(jié)對一個自行研發(fā)的課程管理Web系統(tǒng)中的查詢課程子功能進(jìn)行CPN建模，構(gòu)建得到的應(yīng)用系統(tǒng)CPN模型關(guān)注查詢課程進(jìn)程中的資源交互和通信。如圖7所示，對課程查詢客戶端、課程查詢系統(tǒng)網(wǎng)關(guān)、課程查詢系統(tǒng)服務(wù)器和課程查詢系統(tǒng)數(shù)據(jù)庫之間的通信行為進(jìn)行了建模和分析，并使用基于模型狀態(tài)空間執(zhí)行路徑同步匹配的驗(yàn)證方法確認(rèn)該模型是否滿足REST服務(wù)架構(gòu)的五個標(biāo)準(zhǔn)特征約束。

Figure 7 CPN model of the course query subfunction圖7 課程查詢子功能的CPN模型

該模型中，由課程查詢系統(tǒng)Web用戶發(fā)出查詢請求資源信息msg，該請求信息msg的數(shù)據(jù)定義為colsetMsg1=recordm:MSG*f:FORMAT*s:SENDER*r:RECEIVER，其中MSG、FORMAT、SENDER和RECEIVER均為字符串類型。通過通道ReqCHUG傳送請求信息給課程查詢系統(tǒng)的網(wǎng)關(guān)(Gateway)，然后由網(wǎng)關(guān)通過通道ReqCHGSC傳送請求信息給課程查詢系統(tǒng)服務(wù)器(Server)的緩存中。若該請求資源信息緩存在服務(wù)器的緩存SCache中(用ReqCHGSC變遷出弧表達(dá)式中的第一個元素分量m="1"來示例)，則服務(wù)器通過通道Reply1直接返回消息給該課程查詢系統(tǒng)的用戶；若該課程查詢系統(tǒng)服務(wù)器的緩存中不存在該請求資源(用ReqCHGSC變遷出弧表達(dá)式中的第一個元素分量m="no"來示例)，則通過通道Search發(fā)送請求消息給該課程查詢Web系統(tǒng)的數(shù)據(jù)庫(Database)，然后從數(shù)據(jù)庫中返回請求資源信息給系統(tǒng)用戶。圖8給出了課程查詢子功能的CPN模型對應(yīng)的狀態(tài)空間。

Figure 8 State space of the course query subfunction model圖8 課程查詢子功能模型的狀態(tài)空間

5.2 標(biāo)準(zhǔn)特征約束驗(yàn)證實(shí)例及分析

以圖8給出的課程查詢子功能CPN模型為基礎(chǔ)，通過與3.2節(jié)的五個REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征約束進(jìn)行逐個比較，檢驗(yàn)該課程查詢子功能Web應(yīng)用是否為標(biāo)準(zhǔn)的REST架構(gòu)應(yīng)用。(1)對客戶端服務(wù)器標(biāo)準(zhǔn)特征約束進(jìn)行檢驗(yàn)，通過與3.2.1節(jié)的標(biāo)準(zhǔn)客戶端服務(wù)器約束的狀態(tài)空間執(zhí)行路徑進(jìn)行比對，發(fā)現(xiàn)該REST架構(gòu)模型不滿足客戶端服務(wù)器約束。由模型發(fā)現(xiàn)該應(yīng)用模型的課程查詢系統(tǒng)用戶的功能等價于標(biāo)準(zhǔn)REST架構(gòu)模型中的用戶代理的功能， 該課程查詢系統(tǒng)的網(wǎng)關(guān)功能等價于標(biāo)準(zhǔn)REST架構(gòu)模型中的中間件，該課程查詢系統(tǒng)的服務(wù)器功能等價于標(biāo)準(zhǔn)REST架構(gòu)模型中源服務(wù)器的功能，該課程查詢系統(tǒng)的數(shù)據(jù)庫功能等價于標(biāo)準(zhǔn)REST架構(gòu)模型中的資源的功能。經(jīng)過使用同步路徑匹配算法檢驗(yàn)，圖8中的節(jié)點(diǎn)1與圖9中的節(jié)點(diǎn)1是初始同步節(jié)點(diǎn)，然后經(jīng)過變遷路徑發(fā)現(xiàn)該REST架構(gòu)應(yīng)用模型缺少其客戶端的緩存功能，獲取請求信息時要先看其緩存中是否存在，若不存在則繼續(xù)向源服務(wù)器請求資源信息，故該課程查詢子功能Web系統(tǒng)應(yīng)增加客戶端的緩存功能。

Figure 9 State space of standard client server constraints圖9 標(biāo)準(zhǔn)客戶端服務(wù)器約束狀態(tài)空間圖

Figure 10 State space of standard cachable constraints圖10 標(biāo)準(zhǔn)可緩存約束狀態(tài)空間圖

(2)對可緩存標(biāo)準(zhǔn)特征約束進(jìn)行檢驗(yàn)，通過與3.2.2節(jié)的標(biāo)準(zhǔn)可緩存約束模型的狀態(tài)空間執(zhí)行路徑進(jìn)行比對，發(fā)現(xiàn)該REST架構(gòu)模型不滿足可緩存約束。經(jīng)過使用同步路徑匹配算法檢驗(yàn)，可發(fā)現(xiàn)圖8中的節(jié)點(diǎn)1與圖10中的節(jié)點(diǎn)1是初始同步節(jié)點(diǎn)，從后繼變遷路徑中可發(fā)現(xiàn)該課程查詢系統(tǒng)的用戶端和網(wǎng)關(guān)均缺少緩存功能，故該課程查詢子功能Web系統(tǒng)應(yīng)增加相應(yīng)的緩存機(jī)制。

Figure 11 Corrected CPN model of the course query subfunction圖11 課程查詢子功能的修正CPN模型

(3)對分層標(biāo)準(zhǔn)特征約束進(jìn)行檢驗(yàn)，通過對其狀態(tài)空間執(zhí)行路徑驗(yàn)證，發(fā)現(xiàn)該REST架構(gòu)模型滿足分層約束。通過與3.2.4節(jié)的標(biāo)準(zhǔn)分層約束的狀態(tài)空間執(zhí)行路徑進(jìn)行比對，該課程查詢系統(tǒng)用戶只能通過課程查詢系統(tǒng)的網(wǎng)關(guān)進(jìn)行交互，課程查詢系統(tǒng)的數(shù)據(jù)庫只能和服務(wù)器進(jìn)行通信，該課程查詢子功能Web系統(tǒng)滿足分層標(biāo)準(zhǔn)特征約束。同時,對無狀態(tài)和統(tǒng)一接口標(biāo)準(zhǔn)特征約束進(jìn)行檢驗(yàn)，通過3.2.3節(jié)的標(biāo)準(zhǔn)無狀態(tài)約束的狀態(tài)空間執(zhí)行路徑比對，可以發(fā)現(xiàn)該REST架構(gòu)的課程查詢系統(tǒng)滿足無狀態(tài)約束，消息的所有信息可包含在發(fā)送的請求和回答信息中，主要內(nèi)容存儲在服務(wù)器中，服務(wù)器是無狀態(tài)的；通過與3.2.5節(jié)的標(biāo)準(zhǔn)統(tǒng)一接口約束的狀態(tài)空間執(zhí)行路徑比對，發(fā)現(xiàn)該模型滿足統(tǒng)一接口約束，請求和響應(yīng)的消息格式是一致的，都是msg形式，當(dāng)兩次發(fā)送的請求信息相同時，響應(yīng)信息是相同的，故滿足統(tǒng)一接口約束。

通過以上的分析，圖11給出了修改后的基于REST服務(wù)架構(gòu)的課程查詢子功能應(yīng)用系統(tǒng)的CPN模型，經(jīng)再次使用本文所提方法確認(rèn)，該應(yīng)用系統(tǒng)滿足了REST服務(wù)架構(gòu)的各項(xiàng)標(biāo)準(zhǔn)特征約束。從圖7和圖11的對比分析可看出：(1)圖11比圖7增加了Users Cache緩存功能，其可以為課程管理Web系統(tǒng)的客戶端增加緩存功能；(2)圖11比圖7增加了Gateway Cache緩存功能，其可以為課程管理Web系統(tǒng)的網(wǎng)關(guān)增加緩存功能。增加以上兩個緩存器，使得系統(tǒng)功能更加完善，當(dāng)課程管理Web系統(tǒng)的客戶端發(fā)出請求信息時，首先檢驗(yàn)其內(nèi)部緩存中是否存在該資源，如果其緩存中存在該資源(用ReqCHUC變遷出弧表達(dá)式中的第四個元素分量r="4"來示例)，則直接返回響應(yīng)消息給客戶端；若不存在客戶端緩存中(用ReqCHUC變遷出弧表達(dá)式中的第四個元素分量r="Ucache"來示例)，需要向課程管理Web系統(tǒng)的網(wǎng)關(guān)請求資源，若該資源存在網(wǎng)關(guān)的緩存中(用ReqCHUG變遷出弧表達(dá)式中的第四個元素分量r="Ucache"來示例)，則直接返回響應(yīng)消息給客戶端。

6 結(jié)束語

實(shí)現(xiàn)基于REST服務(wù)架構(gòu)的Web系統(tǒng)前，驗(yàn)證該系統(tǒng)設(shè)計是否滿足REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征是至關(guān)重要的，能夠有效提升基于REST服務(wù)架構(gòu)的Web系統(tǒng)的研發(fā)質(zhì)量。本文提出了一種基于CPN模型的REST服務(wù)架構(gòu)標(biāo)準(zhǔn)特征驗(yàn)證方法。首先，給出了REST服務(wù)架構(gòu)的五個標(biāo)準(zhǔn)特征約束的CPN模型描述，以此為基礎(chǔ)，提出了一種基于模型狀態(tài)空間執(zhí)行路徑同步匹配的驗(yàn)證方法，以應(yīng)用系統(tǒng)的CPN模型和標(biāo)準(zhǔn)特征約束的CPN模型為基礎(chǔ)，對模型狀態(tài)空間中的各自執(zhí)行路徑進(jìn)行同步匹配，若路徑可同步執(zhí)行完畢則說明該應(yīng)用系統(tǒng)滿足該REST標(biāo)準(zhǔn)特征約束。最后，以基于REST服務(wù)架構(gòu)的課程查詢功能系統(tǒng)為實(shí)際應(yīng)用，確認(rèn)了上述驗(yàn)證方法的可用性，應(yīng)用本文所提驗(yàn)證方法可以有效確認(rèn)基于REST服務(wù)架構(gòu)的Web應(yīng)用系統(tǒng)設(shè)計是否符合REST服務(wù)架構(gòu)的標(biāo)準(zhǔn)特征約束，并在不符合標(biāo)準(zhǔn)特征約束時提供直觀、可行的執(zhí)行數(shù)據(jù)，便于后續(xù)完成應(yīng)用系統(tǒng)設(shè)計缺陷定位及修正。下一步工作需強(qiáng)化驗(yàn)證方法核心過程的形式描述和有效性確認(rèn)，并以更多基于REST服務(wù)架構(gòu)的典型應(yīng)用系統(tǒng)為實(shí)踐對象應(yīng)用本方法，完善方法執(zhí)行細(xì)節(jié)，提升方法的可用性。

[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.

附中文參考文獻(xiàn)：

[4] 劉靖,葉新銘,周建濤.復(fù)雜網(wǎng)絡(luò)軟件的著色Petri網(wǎng)層次建模及模型集成確認(rèn)方法[J].高技術(shù)通訊,2013,23(11):1139-1147.

[6] 孫連俠,基于分層著色Petri網(wǎng)的Web服務(wù)動態(tài)組合建模與驗(yàn)證[D].東營：中國石油大學(xué),2011.

[11] 袁婷.RESTful Web服務(wù)的形式化建模與分析[J].上海：華東師范大學(xué),2015.