基于模型檢測的微服務組合平臺QoS驗證

毛昕怡，鈕 俊，丁雪兒，張開樂

（寧波大學信息科學與工程學院，浙江寧波 315211）

（?通信作者電子郵箱niujun@nbu.edu.cn）

0 引言

在應用系統設計及實現中，單體架構模式一般將整個系統視為一個整體進行開發、部署及運行，能較好地適用于小型系統的開發。然而單體架構中各個功能模塊邊界模糊、代碼耦合度高。隨著系統業務功能的不斷擴充，單體應用復雜性高、維護成本大、難以擴展等缺陷愈發明顯。

為了應對上述問題，微服務體系結構（Microservice Architecture，MA）應運而生［1］。MA的基本思想是將單體應用拆分為若干小型微服務，每個微服務職責單一、業務邏輯清晰、結構簡單。整個應用系統的構建則需對已經存在的多個微服務進行組合而得到［2］。微服務架構可使分布式系統具有更好的彈性，已被Amazon、Netflix、Uber 等公司作為業務系統架構的首選解決方案［3］。與單體架構相比，微服務架構需針對用戶業務請求靈活、快速、準確地生成組合微服務。如何確保微服務組合過程的快速響應已受到學術界、工程界廣泛關注［4］。

目前已存在不少針對微服務組合平臺性能分析方法的有關研究：文獻［5］闡述了對微服務組合系統性能進行預測分析的必要性，并預測了相關的研究方向；文獻［6］分析了微服務組合平臺的參與組件如容器、虛擬機和服務提供者的忙閑狀態，進而分析了整個組合平臺的狀態劃分及轉換過程；文獻［7］研究了影響服務請求等待隊列長度閾值設定的因素并給出防止等待隊列過載的策略；文獻［8］提出一種微服務組合平臺的性能評價模型，可用于分析微服務平臺的各項性能指標，但該方法未充分考慮服務請求的異構性，如服務實例個數的差異等。

可以看出，已有工作主要對影響微服務組合平臺性能的因素進行了研究，給出對相關性質進行分析和預測的方法，而并未結合組合過程的正確性全方位地考察其有效性。本文借助具有自動、完備等優點的模型檢測技術（Model checking）來形式化地分析微服務組合平臺的可靠性。該技術是一種窮盡搜索模型狀態的形式化驗證技術［4］。

本文考慮了組合服務的特性、服務調度方法以及資源提供策略等對性能的影響，以微服務組合平臺作為研究對象建立形式模型，并通過模型檢測技術對服務請求的響應時間、請求丟失率和資源利用率等服務質量（Quality of Service，QoS）指標進行驗證。具體方法包括3 個步驟：1）提出一個用以描述微服務資源配置過程的概率模型；2）通過概率時序邏輯公式刻畫待驗證的QoS 性質；3）通過實驗來檢測方法可支持的數據規模，并分析得到的驗證結果，以說明方法的可行性。方法框架如圖1所示。

圖1 所提方法框架Fig.1 Framework of the proposed method

1 微服務組合平臺資源調配過程

在微服務實現框架中，一般通過容器技術將運行實例及所需的運行組件封裝在一起，并在虛擬機中以輕量級進程方式實現快速部署和運維［9］。網關在收到用戶的請求后，通過配置器向虛擬機申請容器資源以部署各微服務的運行實例，并通過聚合器將各微服務組合起來［10］，如圖2所示。

圖2 微服務的組合Fig.2 Microservice composition

從抽象角度看，微服務平臺資源調配過程實質上就是為客戶請求提供所需容器，服務運行結束后再回收其所占容器的過程，即容器資源的分配與回收。因此本文參考了Khazaei等［11］提出的對分布式云計算中心的服務資源分配過程建模的方法，將微服務平臺容器配置過程劃分為請求到達階段、資源配置階段和服務執行階段。在請求到達階段，配置器需對當前虛擬機中可用容器的數量能否滿足請求的需要進行判斷。新到達的請求如果能被立即處理，則根據一定規則分配容器供其運行，用戶請求進入資源配置階段，否則停留在等待隊列中。如果隊列中的請求總數超過某個閾值，新到來的請求將會被拒絕。資源配置成功的服務請求將獲得所需資源進入服務執行階段，執行完成后釋放所占資源，如圖3所示。

圖3 請求的執行過程Fig.3 Execution procedure of request

為了方便模型建立，應先給出相關參數的具體描述及表示。設等待隊列中可接受服務請求的最大數目為K、虛擬機中可部署容器數量為N。設服務請求到達率為λ，即服務請求到達的時間間隔獨立且服從參數為的指數分布。設配置器執行配置任務的執行速率為γ，服務執行時間服從參數為μ的負指數分布。假定當前虛擬機中正在執行的服務請求數為r，可用容器數為m。為方便描述，本文僅以服務請求所需容器資源數量的不同作為劃分請求類型的依據，以x 表示請求所需的容器數。模型涉及的參數符號及其含義如表1所示。

表1 參數表示及含義Tab.1 Symbols and meanings

2 基于Markov鏈的微服務組合平臺建模

為了分析微服務組合平臺相關性能參數，首先需要構建其形式化模型。由于服務請求到達時刻及請求需要的容器數量等都存在不確定性，因此它們的動態行為過程可描述為狀態離散、時間連續且具有Markov 性的系統。沿用已有文獻［10］中對微服務組合過程的分析，本文基于連續時間Markov鏈（Continuous-Time Markov Chain，CTMC）來對各個組件進行建模［12］。同時，為了更為全面地分析各個組件與狀態相關聯的量化性能參數，本文為CTMC 的狀態以及狀態的轉移設置獎勵回報值（Reward），以描述相關性能參數的大小。

2.1 基本描述及定義

為了能夠對CTMC 的狀態進行推理，需要為每個狀態添加命題標記。本文將增加了回報函數和命題標記的CTMC 模型命名為帶標記Markov 回報模型（Labelled Markov Reward Model，LMRM）［13］，具體定義如下。

定義1帶標記Markov 回報模型。設R≥0為非負實數集，AP 為原子命題有限集，用于標識CTMC 的狀態，模型LMRM 可用六元組M=（S，sinit，L，R，RoS，RoT）表示，其中：S 為有限狀態集；sinit∈S 代表初始狀態；L：S→2AP為狀態標記函數，定義為在各個狀態上成立的原子命題集合為轉移率矩陣為狀態回報函數為轉移回報函數。

對于s1、s2∈S，如果R（s1，s2）＞0，則存在從s1到s2的轉移，且轉移的延遲時間滿足參數為R（s1，s2）的指數分布。如果對任意狀態s'都有R（s，s'）=0，即不存在從狀態s 出發的任何轉移，則稱s 為吸收狀態。如果存在多個狀態s'滿足R（s，s'）＞0，這種情形下狀態s 的后繼狀態選擇的概率，需要借助狀態的離開速率E（s）來表述和計算，其中在時間t 內離開狀態s 的概率為1-e-E(s)?t，且在時間t 內轉移到狀態s'的概率如式（1）所示：

系統執行過程中，狀態轉移的序列可以用路徑來表示，LMRM模型中的路徑定義如下。

定義2路徑Path。LMRM 中的路徑是狀態、時間的序列，一個無限路徑可表示為序列：

其中路徑中任意的狀態si都滿足i ∈N 且表示狀態si持續的時間。一個有限路徑可表示為序列：

對于路徑中任意的狀態si都滿足i ∈N 且R（si，si+1）＞0，其中sn為吸收狀態。

將路徑中的回報值累加起來，可得到一個與路徑有關的度量值，稱為累積回報。例如在驗證請求拒絕率時，給拒絕請求的狀態轉移賦值為1，則一定時間范圍內，某條路徑上該回報值的累加，即為該時間范圍內被拒絕的請求總數。以RoS(s)表示在狀態s下單位時間內的回報值，如果一個狀態持續時間為t（s），則該狀態累計回報值是t(s) × RoS(s)，以RoT(s，s')表示發生從狀態s到狀態s'的轉移時的回報值，則路徑上從狀態a 到狀態b 的路徑片段上的累積回報為所有狀態的累計回報和所有轉移上的回報值之和如式（2）所示：

通過搜尋并計算每條路徑中的累積回報值，可得到從狀態s 出發的所有路徑，作為與路徑相關的模型屬性的樣本空間。

2.2 微服務組合平臺模型

對微服務組合平臺進行建模時，需將隨機系統拆分為等待隊列模塊、配置器模塊以及虛擬機模塊分別進行建模。模塊的具體行為由一組進程代數形式的行為標簽來標記。行為標簽可強制多個模塊在滿足條件時同步發生狀態轉移。當兩個模塊間發生同步狀態轉移時，以其中一個模塊的行為作為主動轉移，轉移速率記為參數lambda，另一個模塊的行為視作被動轉移，轉移速率記為1，則同步轉移的發生速率為兩個單獨速率的乘積lambda*1。模塊狀態由局部變量來定義，模型的整體狀態根據各個模塊的局部變量和系統的全局變量來評估。首先通過LMRM模型對3個模塊分別進行建模。

2.2.1 等待隊列模塊

當新請求到達而不能被立刻處理時，該請求將進入等待隊列，隊列長度增加。當配置器完成某個資源配置任務，將按照先進先出原則對等待隊列首位的請求進行配置決策。只有滿足決策條件：虛擬機中可部署容器的數量大于請求所需容器個數時，該請求才進入配置階段，等待隊列長度減小。若等待隊列已滿，新到達的請求將會被拒絕。本文用等待隊列中請求數量來標識該模塊的不同狀態，設等待隊列最多可容納請求數為K，則等待隊列模塊有K+1 個狀態，記為狀態集S=｛w0，w1，…，wK｝，其中wi表示等待隊列中當前請求數為i（0≤i≤K）。當新的請求達到或配置器完成請求配置時，都可能引起等待隊列狀態變化，下面具體描述其狀態轉移過程。

設請求到達服從參數為λ 的泊松分布，當前狀態為wi，則當新請求到達時，如果i=0，即等待隊列為空，如果該請求能夠立即被處理，則存在一個轉移速率為λ，到狀態w0自身的轉移，否則以速率λ從狀態w0轉移到狀態w1，將該行為標簽記為［rq_0］。如果0＜i＜K，則將以速率λ 從狀態wi轉移到狀態wi+1，將該行為標簽記為［rq］。如果i=K，即等待隊列已滿，新請求將被拒絕，則存在一個轉移速率為λ，到狀態wK自身的轉移，將該行為標簽記為［lose］。

當配置器完成當前任務，將完成配置任務的行為標簽記為［dp］。等待隊列模塊將在［dp］上發生被動轉移，故轉移速率為1。如果等待隊列中當前請求數大于0，應先進行配置決策。只有請求滿足決策條件才能進入配置階段，模塊狀態從wi轉移至狀態wi-1；否則請求將繼續等待，即發生一個到狀態wi自身的轉移。等待隊列模塊的狀態轉移過程如圖4所示。

圖4 等待隊列模塊的狀態轉移過程Fig.4 State transition process of queuing module

2.2.2 配置器模塊

配置器對待處理的請求進行配置決策，并對滿足決策條件的請求分配所需的容器資源。當配置器與等待隊列中都沒有請求需要處理時，配置模塊處在空閑狀態，如果當前有新請求到達且滿足決策條件，則配置器為其分配及部署容器，狀態進入工作狀態；否則配置器需要在有請求執行完成并釋放占用的容器資源時，反復進行決策，直至決策條件滿足，該狀態稱為決策狀態。以d0表示空閑狀態，d1表示決策狀態，d2表示工作狀態。設配置器模塊的狀態集為S=｛d0，d1，d2｝，顯然，當新的請求達到、配置器完成當前請求的配置或者有服務執行完成時，都可能引起配置器模塊的狀態變化。下面具體描述其狀態轉移過程。

當新請求到達且等待隊列為空時，配置器模塊將在行為標簽［rq_0］上發生被動轉移，轉移速率為1。若當前狀態為不為d0，則發生一個到狀態本身的轉移；若當前狀態為d0，即配置器處在空閑狀態，則應先對到達的服務請求進行配置決策，如果滿足決策條件，狀態轉移至d2，否則狀態轉移至d1。

設配置器執行速率為γ。當前配置任務完成時，如果此時還有請求等待且滿足決策條件，則請求進入配置階段，發生一個到狀態本身的轉移，否則請求需繼續等待，狀態轉移到d1。如果等待隊列為空，則狀態轉移到d2。將該行為標簽記為［dp］。

當虛擬機模塊中有服務執行完成時，執行完成的請求釋放占用的資源，將該行為標簽記為［sv］。配置器模塊將在行為標簽［sv］上發生被動轉移，轉移速率為1。如果此時狀態為d1且滿足決策條件，則待配置的請求可進入配置階段，狀態轉移到d2，否則發生一個到狀態本身d1的轉移。

配置器模塊的狀態轉移過程如圖5所示。

圖5 配置器模塊的狀態轉移過程Fig.5 State transition process of configulator module

2.2.3 虛擬機模塊

服務請求配置完成之后，將在虛擬機中進行服務的部署、啟動與執行。虛擬機模塊的狀態可以用一個二元組V=（r，m）來描述，其中，r表示正在執行中的服務請求數，m 表示剩余可部署的容器數。當需要x 個容器的服務請求配置完成，虛擬機中剩余可部署的容器數將減少x，正在執行中的服務請求數加1。當服務請求執行完成，將會釋放占用的容器資源并離開系統，剩余可部署的容器數將增加x，正在執行中的服務請求減1。設虛擬機中最多可部署容器個數為N，當前狀態為（i，j），當前配置任務完成或有服務執行完成時，都將會引起狀態變化。下面具體描述其狀態轉移過程。

當有服務執行完成時，設執行請求花費的時間服從參數為μ 的負指數分布，如果執行完成的請求類型為x，則系統狀態以速率μ轉移到（i -1，j+x），該行為標簽記為［sv］。

當前配置任務完成時，虛擬機模塊將在行為標簽［dp］上發生被動轉移，轉移速率為1，狀態轉移到（i+1，j-x）。

虛擬機模塊的狀態轉移過程如圖6所示。

圖6 虛擬機模塊的狀態轉移過程Fig.6 State transition process of virtual machine module

3 連續隨機邏輯語法和語義

第2 章已經構造出微服務平臺中各個組件運行過程的概率模型，還需要借助時序邏輯公式來嚴謹地刻畫待驗證的性質［14］，其中連續隨機邏輯公式（Continuous Stochastic Logic，CSL）能夠描述CTMC 模型中的時間連續性和概率特征，故采用CSL對待驗證的屬性進行描述。本文將增加了獎勵回報的CSL 命名為連續隨機回報邏輯公式（Continuous Stochastic Reward Logic，CSRL）［15］，首先給出CSRL的語法定義。

定義3CSRL 語法。設φ 為連續時間Markov 鏈上的狀態公式，φ 為路徑公式，則Markov 鏈模型上的狀態公式、路徑公式可分別定義為：

式中：a ∈AP 為原子命題，?∈{＞，＜，≥，≤}，p∈［0，1］，I 與J為非負實區間，I表示某個時間間隔，J表示時間間隔內累積回報值的區間，?p 用于限定概率范圍為瞬時概率算子為穩態概率算子，操作符X和U 是標準的時序邏輯操作符，用于刻畫Markov鏈中的路徑應該滿足的性質，其中X代表“下一個”，U 代表“直到”。為了在Markov 鏈模型中對相關的CSRL 性質進行推理，必須給出CSRL 邏輯公式可滿足語義的定義。

定義4CSRL 語義。定義一個LMRM 為M=（S，sinit，L，R，RoS，RoT），在CSRL 公式中，若其中狀態s滿足狀態公式φ，則表示為M，s ?φ。CSRL狀態公式可滿足語義定義如下：

其中：SatM(φ)={s ∈S|M，s ?φ}表示在M 中滿足狀態公式φ的狀態集合；πM(s，SatM(φ))描述由狀態s開始的穩定狀態下，滿足公式φ 的概率；ProbM（s，φ）表示從狀態s 出發的所有路徑都滿足路徑公式φ 的概率，以PathM（s）表示M 中的有限路徑集合，可得到式（11）：

PRISM 是一個用于建模和分析隨機系統的模型檢測工具，由英國伯明翰大學的Kwiatkowska 教授負責的研究小組開發，其本身支持模型的定量驗證，使用CSRL 可以驗證具體概率值的大小，同時也可以得到模型在運行中的最大值、最小值等量化數據［16］。在PRISM 屬性規約語言中，P 操作符用于推算事件發生的概率，如果從狀態s 出發的路徑滿足路徑屬性“pathprop”的概率在給定范圍之內，那么該屬性為true。P 操作符除了能夠驗證路徑屬性的概率是否落在給定的范圍內，還可計算一些模型行為的真實概率并返回具體數值，表示為P=？［pathprop］。R操作符可用于分析計算與回報值相關的屬性。從狀態s出發的路徑滿足回報屬性“rewardprop”的累積回報值，表示為R query［rewardprop］，其中query 可表示為“=？”“min=？”或者“max=？”。

4 實驗及結果分析

為了驗證上述方法的可適用性，本章將對一個微服務組合平臺的資源配置過程進行建模分析，并設計了3 個實驗：實驗1 以虛擬機中的容器總數為變量參數，驗證在不同容器總數下，等待隊列的平均長度，并檢測方法可支持的數據規模；實驗2 通過改變運行的時間區間大小，來研究運行時間長短對驗證效率及驗證結果的影響；實驗3 通過對更為復雜的請求丟失率、虛擬機資源利用率等性質進行驗證，進一步說明方法的可適用性。

4.1 實驗配置及參數

本文實驗的運行環境為Windows 10 系統，Intel Core i7-7700 CPU 3.60 GHz 處理器，16.0 GB 內存，實驗工具為概率模型檢測器PRISM，版本號為4.5。

本文以基于微服務的在線購物平臺作為研究對象，將資源配置過程抽象出來建模成LMRM 模型，并通過檢測工具PRISM 對期望檢驗的性質進行實驗分析。在線購物平臺包含4 個主要的服務功能：商品服務、購物車服務、訂單服務和個人中心服務。假設在該場景下的商品服務由3 個子微服務組合完成，且被調用的概率占所有服務請求的1/2；購物車服務由4 個子微服務組合完成，且被調用的概率占所有服務請求的1/4；訂單服務由5 個子微服務組合完成，且被調用的概率占所有服務請求的3/16；個人信息服務由4 個子微服務組合完成，且被調用的概率占所有服務請求的1/16。表2列出了各服務功能的基本參數。

表2 不同類型的服務參數Tab.2 Different types of service parameters

實驗中請求數量、請求處理速率及虛擬機規模等常量的取值參考了文獻［8］，將本文實驗得到的驗證結果與通過文獻［8］中建模與驗證方法獲得的實驗結果做對比，可進一步證明方法的可靠性。

4.2 實驗1

模型檢測的原理是對模型的狀態空間進行遍歷搜索，因此具有自動化程度高、保證驗證結果正確等優點，然而隨著系統規模的擴大，其狀態數會呈指數增長，容易產生狀態爆炸的問題。為了確保實驗的順利進行，首先需要對模型可支持的數據規模進行檢測。實驗1 以虛擬機中一共能部署的容器數量N 為變量，對不同N 取值下的模型狀態數、轉移數及驗證耗費的時長等進行檢測，以驗證模型可支持的數據規模。

將等待隊列長度的獎勵回報函數標簽記為“queue_size”，從0時刻開始的T個單位時間內，系統的平均等待隊列長度的CSRL描述如式（12）：

設等待隊列一共能接受的請求個數K 為10，請求到達速率λ 的數值為8，請求配置速率γ 的數值為10，微服務執行完成速率μ 的數值為3。將變量N 在30～70 每隔10 取一點作為參數，測試在T=100 個單位時間內等待隊列的平均長度。驗證花費的時間取決于實驗設備的數據處理能力，在本文實驗環境下驗證結果及模型的狀態數、轉移數和驗證所花費的時長記錄如表3。

表3 實驗1驗證結果Tab.3 Verification results of experiment 1

由表3 可知，隨著虛擬機內可部署容器數量的增加等待隊列的平均長度逐漸變短，與實際運行情況相符，說明了本文方法的可行性；且系統狀態數隨著容器數量的增加而增加，當N 為70 時，驗證用時才有大幅度的增加。N 為90 時，雖然驗證已需要花費較高的時間成本，但依然能夠給出準確的驗證結果，說明本文方法可用于狀態數較多的模型驗證。

4.3 實驗2

實驗2 在實驗1 的基礎上，對更為復雜的系統性能指標：虛擬機中資源的利用率進行驗證。設資源利用率的獎勵回報函數標簽記為“utilization”，從0時刻開始的T個單位時間內虛擬機中容器資源的利用率的CSRL描述如式（13）：

實驗2 以N 為變量，在40～80 每隔10 取一點作為變量N的參數進行測試，常量取值與實驗1 相同。在對不同N 的取值進行實驗時，從數值0～100 內每隔10 個單位時間取一點為參數進行驗證，以模擬虛擬機中資源利用率隨系統運行的變化。PRISM 可根據設定參數自動生成驗證結果的折線圖如圖7所示。

圖7 實驗2驗證結果Fig.7 Verification results of experiment 2

由圖7 可知，在不同的虛擬機容量下，資源利用率隨著系統運行時間的增加而發生的變化。虛擬機的容量越小，資源利用率就越高，且在越小的容量下，資源利用率隨運行時間變化增加的幅度就越大。到100 個時間單位時變化幅度基本趨于穩定，即運行中的微服務組合平臺的資源利用率一般維持在0.9 左右，變化曲線與現有研究中的實驗結果相似，且與實際運行情況相符。

4.4 實驗3

對虛擬機資源利用率的驗證只涉及一個獎勵回報函數“utilization”，而驗證另外一些性能指標時可能涉及多個獎勵回報函數。如驗證一個時間間隔內服務請求的拒絕率，需要涉及被拒絕的服務請求數和服務請求總數兩個獎勵回報函數。將被拒絕的服務請求數的獎勵回報函數標簽記為“lose”，服務請求總數的獎勵回報函數標簽記為“quest”，從0 時刻開始的T個單位時間內的請求拒絕率用CSRL描述如式（14）：

實驗3 以N 為變量，在40～80 每隔10 取一點作為變量N的參數進行測試，常量取值與實驗1 相同。在對不同N 的取值進行實驗時，從數值0～200 內每隔10 個單位時間取一點為參數進行驗證，驗證結果如圖8所示。

由圖8 可知，隨著虛擬機的容量增大，服務被拒絕的概率降低，且請求拒絕率在系統運行一段時間之后逐漸趨于穩定，請求拒絕率的變化曲線與文獻［8］中的變化曲線相似，且與實際運行情況相符。

圖8 實驗3驗證結果Fig.8 Verification results of experiment 3

5 結語

本文提出一種基于概率模型檢測的微服務組合平臺性能評估方法。首先，對微服務平臺中的服務組合及資源配置過程進行描述，并將整體系統拆分為三個子模塊：等待隊列模塊、配置器模塊、虛擬機模塊，采用概率模型LMRM 對三個子模塊分別進行建模；接著，用概率邏輯公式CSRL 對待測性質進行刻畫；最后，設計一個在線購物平臺的實例，使用檢測工具PRISM 對平臺性能進行模擬驗證，驗證了方法可支持的數據規模、對復雜性質進行驗證的可行性等，以證明方法的可行性。下一步工作將考慮更加復雜的請求調度情形，同時進一步簡化模型以減少系統狀態數量。