趙玉強,劉 靖

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

1 引言

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

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

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

2 相關工作基礎

2.1 REST服務架構的基本概念

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

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

2.2 CPN方法概述

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

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

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服務的無狀態(tài)等屬性進行描述，并基于PAT工具進行驗證。此外，文獻[12]使用層次CPN對Web Services系統(tǒng)模型進行行為模擬，并基于生成的狀態(tài)空間完成功能驗證，主要是證明Web Services擴展模型可以提高信息的通信傳輸性能。通過以上研究可知，使用CPN模型對Web應用系統(tǒng)進行建模、分析和驗證是可行的。

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

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

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

3.2 基于CPN模型的REST服務架構標準特征約束建模

3.2.1 客戶端-服務器約束

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

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

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

3.2.2 可緩存約束

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

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

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

3.2.3 無狀態(tài)約束

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

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

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

3.2.4 分層約束

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

圖5給出了REST架構的分層標準特征約束模型。

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

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

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

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

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

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

4 REST服務架構標準特征驗證方法

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

4.1 驗證方法的基本思想

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

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

4.2 驗證方法的算法描述

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

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

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

AlgorithmSynchronizedPathMatch{

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

While(i

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

Find the initial synchronization node；

}

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

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

k=1;//k指標準特征約束模型節(jié)點和路徑編號

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

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

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

Find the next synchronization node；

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

else

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

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

Find the synchronization node;}

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

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

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

}}

5 REST服務架構標準特征驗證方法的實例應用

本節(jié)以基于REST服務架構的課程管理Web系統(tǒng)為例，驗證上一節(jié)給出的驗證方法的可用性和有效性，確認本文所提驗證方法可以用于檢驗基于REST服務架構的Web應用系統(tǒng)設計是否符合REST服務架構的標準特征約束。

5.1 基于REST服務架構的Web應用系統(tǒng)建模

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

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)關(Gateway)，然后由網(wǎng)關通過通道ReqCHGSC傳送請求信息給課程查詢系統(tǒng)服務器(Server)的緩存中。若該請求資源信息緩存在服務器的緩存SCache中(用ReqCHGSC變遷出弧表達式中的第一個元素分量m="1"來示例)，則服務器通過通道Reply1直接返回消息給該課程查詢系統(tǒng)的用戶；若該課程查詢系統(tǒng)服務器的緩存中不存在該請求資源(用ReqCHGSC變遷出弧表達式中的第一個元素分量m="no"來示例)，則通過通道Search發(fā)送請求消息給該課程查詢Web系統(tǒng)的數(shù)據(jù)庫(Database)，然后從數(shù)據(jù)庫中返回請求資源信息給系統(tǒng)用戶。圖8給出了課程查詢子功能的CPN模型對應的狀態(tài)空間。

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

5.2 標準特征約束驗證實例及分析

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

Figure 9 State space of standard client server constraints圖9 標準客戶端服務器約束狀態(tài)空間圖

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

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

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

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

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

6 結束語

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

附中文參考文獻：

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

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

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