基于模型檢測(cè)的微服務(wù)組合平臺(tái)QoS驗(yàn)證

毛昕怡，鈕 俊，丁雪兒，張開(kāi)樂(lè)

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

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

0 引言

在應(yīng)用系統(tǒng)設(shè)計(jì)及實(shí)現(xiàn)中，單體架構(gòu)模式一般將整個(gè)系統(tǒng)視為一個(gè)整體進(jìn)行開(kāi)發(fā)、部署及運(yùn)行，能較好地適用于小型系統(tǒng)的開(kāi)發(fā)。然而單體架構(gòu)中各個(gè)功能模塊邊界模糊、代碼耦合度高。隨著系統(tǒng)業(yè)務(wù)功能的不斷擴(kuò)充，單體應(yīng)用復(fù)雜性高、維護(hù)成本大、難以擴(kuò)展等缺陷愈發(fā)明顯。

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

目前已存在不少針對(duì)微服務(wù)組合平臺(tái)性能分析方法的有關(guān)研究：文獻(xiàn)［5］闡述了對(duì)微服務(wù)組合系統(tǒng)性能進(jìn)行預(yù)測(cè)分析的必要性，并預(yù)測(cè)了相關(guān)的研究方向；文獻(xiàn)［6］分析了微服務(wù)組合平臺(tái)的參與組件如容器、虛擬機(jī)和服務(wù)提供者的忙閑狀態(tài)，進(jìn)而分析了整個(gè)組合平臺(tái)的狀態(tài)劃分及轉(zhuǎn)換過(guò)程；文獻(xiàn)［7］研究了影響服務(wù)請(qǐng)求等待隊(duì)列長(zhǎng)度閾值設(shè)定的因素并給出防止等待隊(duì)列過(guò)載的策略；文獻(xiàn)［8］提出一種微服務(wù)組合平臺(tái)的性能評(píng)價(jià)模型，可用于分析微服務(wù)平臺(tái)的各項(xiàng)性能指標(biāo)，但該方法未充分考慮服務(wù)請(qǐng)求的異構(gòu)性，如服務(wù)實(shí)例個(gè)數(shù)的差異等。

可以看出，已有工作主要對(duì)影響微服務(wù)組合平臺(tái)性能的因素進(jìn)行了研究，給出對(duì)相關(guān)性質(zhì)進(jìn)行分析和預(yù)測(cè)的方法，而并未結(jié)合組合過(guò)程的正確性全方位地考察其有效性。本文借助具有自動(dòng)、完備等優(yōu)點(diǎn)的模型檢測(cè)技術(shù)（Model checking）來(lái)形式化地分析微服務(wù)組合平臺(tái)的可靠性。該技術(shù)是一種窮盡搜索模型狀態(tài)的形式化驗(yàn)證技術(shù)［4］。

本文考慮了組合服務(wù)的特性、服務(wù)調(diào)度方法以及資源提供策略等對(duì)性能的影響，以微服務(wù)組合平臺(tái)作為研究對(duì)象建立形式模型，并通過(guò)模型檢測(cè)技術(shù)對(duì)服務(wù)請(qǐng)求的響應(yīng)時(shí)間、請(qǐng)求丟失率和資源利用率等服務(wù)質(zhì)量（Quality of Service，QoS）指標(biāo)進(jìn)行驗(yàn)證。具體方法包括3 個(gè)步驟：1）提出一個(gè)用以描述微服務(wù)資源配置過(guò)程的概率模型；2）通過(guò)概率時(shí)序邏輯公式刻畫(huà)待驗(yàn)證的QoS 性質(zhì)；3）通過(guò)實(shí)驗(yàn)來(lái)檢測(cè)方法可支持的數(shù)據(jù)規(guī)模，并分析得到的驗(yàn)證結(jié)果，以說(shuō)明方法的可行性。方法框架如圖1所示。

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

1 微服務(wù)組合平臺(tái)資源調(diào)配過(guò)程

在微服務(wù)實(shí)現(xiàn)框架中，一般通過(guò)容器技術(shù)將運(yùn)行實(shí)例及所需的運(yùn)行組件封裝在一起，并在虛擬機(jī)中以輕量級(jí)進(jìn)程方式實(shí)現(xiàn)快速部署和運(yùn)維［9］。網(wǎng)關(guān)在收到用戶(hù)的請(qǐng)求后，通過(guò)配置器向虛擬機(jī)申請(qǐng)容器資源以部署各微服務(wù)的運(yùn)行實(shí)例，并通過(guò)聚合器將各微服務(wù)組合起來(lái)［10］，如圖2所示。

圖2 微服務(wù)的組合Fig.2 Microservice composition

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

圖3 請(qǐng)求的執(zhí)行過(guò)程Fig.3 Execution procedure of request

為了方便模型建立，應(yīng)先給出相關(guān)參數(shù)的具體描述及表示。設(shè)等待隊(duì)列中可接受服務(wù)請(qǐng)求的最大數(shù)目為K、虛擬機(jī)中可部署容器數(shù)量為N。設(shè)服務(wù)請(qǐng)求到達(dá)率為λ，即服務(wù)請(qǐng)求到達(dá)的時(shí)間間隔獨(dú)立且服從參數(shù)為的指數(shù)分布。設(shè)配置器執(zhí)行配置任務(wù)的執(zhí)行速率為γ，服務(wù)執(zhí)行時(shí)間服從參數(shù)為μ的負(fù)指數(shù)分布。假定當(dāng)前虛擬機(jī)中正在執(zhí)行的服務(wù)請(qǐng)求數(shù)為r，可用容器數(shù)為m。為方便描述，本文僅以服務(wù)請(qǐng)求所需容器資源數(shù)量的不同作為劃分請(qǐng)求類(lèi)型的依據(jù)，以x 表示請(qǐng)求所需的容器數(shù)。模型涉及的參數(shù)符號(hào)及其含義如表1所示。

表1 參數(shù)表示及含義Tab.1 Symbols and meanings

2 基于Markov鏈的微服務(wù)組合平臺(tái)建模

為了分析微服務(wù)組合平臺(tái)相關(guān)性能參數(shù)，首先需要構(gòu)建其形式化模型。由于服務(wù)請(qǐng)求到達(dá)時(shí)刻及請(qǐng)求需要的容器數(shù)量等都存在不確定性，因此它們的動(dòng)態(tài)行為過(guò)程可描述為狀態(tài)離散、時(shí)間連續(xù)且具有Markov 性的系統(tǒng)。沿用已有文獻(xiàn)［10］中對(duì)微服務(wù)組合過(guò)程的分析，本文基于連續(xù)時(shí)間Markov鏈（Continuous-Time Markov Chain，CTMC）來(lái)對(duì)各個(gè)組件進(jìn)行建模［12］。同時(shí)，為了更為全面地分析各個(gè)組件與狀態(tài)相關(guān)聯(lián)的量化性能參數(shù)，本文為CTMC 的狀態(tài)以及狀態(tài)的轉(zhuǎn)移設(shè)置獎(jiǎng)勵(lì)回報(bào)值（Reward），以描述相關(guān)性能參數(shù)的大小。

2.1 基本描述及定義

為了能夠?qū)TMC 的狀態(tài)進(jìn)行推理，需要為每個(gè)狀態(tài)添加命題標(biāo)記。本文將增加了回報(bào)函數(shù)和命題標(biāo)記的CTMC 模型命名為帶標(biāo)記Markov 回報(bào)模型（Labelled Markov Reward Model，LMRM）［13］，具體定義如下。

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

對(duì)于s1、s2∈S，如果R（s1，s2）＞0，則存在從s1到s2的轉(zhuǎn)移，且轉(zhuǎn)移的延遲時(shí)間滿(mǎn)足參數(shù)為R（s1，s2）的指數(shù)分布。如果對(duì)任意狀態(tài)s'都有R（s，s'）=0，即不存在從狀態(tài)s 出發(fā)的任何轉(zhuǎn)移，則稱(chēng)s 為吸收狀態(tài)。如果存在多個(gè)狀態(tài)s'滿(mǎn)足R（s，s'）＞0，這種情形下?tīng)顟B(tài)s 的后繼狀態(tài)選擇的概率，需要借助狀態(tài)的離開(kāi)速率E（s）來(lái)表述和計(jì)算，其中在時(shí)間t 內(nèi)離開(kāi)狀態(tài)s 的概率為1-e-E(s)?t，且在時(shí)間t 內(nèi)轉(zhuǎn)移到狀態(tài)s'的概率如式（1）所示：

系統(tǒng)執(zhí)行過(guò)程中，狀態(tài)轉(zhuǎn)移的序列可以用路徑來(lái)表示，LMRM模型中的路徑定義如下。

定義2路徑Path。LMRM 中的路徑是狀態(tài)、時(shí)間的序列，一個(gè)無(wú)限路徑可表示為序列：

其中路徑中任意的狀態(tài)si都滿(mǎn)足i ∈N 且表示狀態(tài)si持續(xù)的時(shí)間。一個(gè)有限路徑可表示為序列：

對(duì)于路徑中任意的狀態(tài)si都滿(mǎn)足i ∈N 且R（si，si+1）＞0，其中sn為吸收狀態(tài)。

將路徑中的回報(bào)值累加起來(lái)，可得到一個(gè)與路徑有關(guān)的度量值，稱(chēng)為累積回報(bào)。例如在驗(yàn)證請(qǐng)求拒絕率時(shí)，給拒絕請(qǐng)求的狀態(tài)轉(zhuǎn)移賦值為1，則一定時(shí)間范圍內(nèi)，某條路徑上該回報(bào)值的累加，即為該時(shí)間范圍內(nèi)被拒絕的請(qǐng)求總數(shù)。以RoS(s)表示在狀態(tài)s下單位時(shí)間內(nèi)的回報(bào)值，如果一個(gè)狀態(tài)持續(xù)時(shí)間為t（s），則該狀態(tài)累計(jì)回報(bào)值是t(s) × RoS(s)，以RoT(s，s')表示發(fā)生從狀態(tài)s到狀態(tài)s'的轉(zhuǎn)移時(shí)的回報(bào)值，則路徑上從狀態(tài)a 到狀態(tài)b 的路徑片段上的累積回報(bào)為所有狀態(tài)的累計(jì)回報(bào)和所有轉(zhuǎn)移上的回報(bào)值之和如式（2）所示：

通過(guò)搜尋并計(jì)算每條路徑中的累積回報(bào)值，可得到從狀態(tài)s 出發(fā)的所有路徑，作為與路徑相關(guān)的模型屬性的樣本空間。

2.2 微服務(wù)組合平臺(tái)模型

對(duì)微服務(wù)組合平臺(tái)進(jìn)行建模時(shí)，需將隨機(jī)系統(tǒng)拆分為等待隊(duì)列模塊、配置器模塊以及虛擬機(jī)模塊分別進(jìn)行建模。模塊的具體行為由一組進(jìn)程代數(shù)形式的行為標(biāo)簽來(lái)標(biāo)記。行為標(biāo)簽可強(qiáng)制多個(gè)模塊在滿(mǎn)足條件時(shí)同步發(fā)生狀態(tài)轉(zhuǎn)移。當(dāng)兩個(gè)模塊間發(fā)生同步狀態(tài)轉(zhuǎn)移時(shí)，以其中一個(gè)模塊的行為作為主動(dòng)轉(zhuǎn)移，轉(zhuǎn)移速率記為參數(shù)lambda，另一個(gè)模塊的行為視作被動(dòng)轉(zhuǎn)移，轉(zhuǎn)移速率記為1，則同步轉(zhuǎn)移的發(fā)生速率為兩個(gè)單獨(dú)速率的乘積lambda*1。模塊狀態(tài)由局部變量來(lái)定義，模型的整體狀態(tài)根據(jù)各個(gè)模塊的局部變量和系統(tǒng)的全局變量來(lái)評(píng)估。首先通過(guò)LMRM模型對(duì)3個(gè)模塊分別進(jìn)行建模。

2.2.1 等待隊(duì)列模塊

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

設(shè)請(qǐng)求到達(dá)服從參數(shù)為λ 的泊松分布，當(dāng)前狀態(tài)為wi，則當(dāng)新請(qǐng)求到達(dá)時(shí)，如果i=0，即等待隊(duì)列為空，如果該請(qǐng)求能夠立即被處理，則存在一個(gè)轉(zhuǎn)移速率為λ，到狀態(tài)w0自身的轉(zhuǎn)移，否則以速率λ從狀態(tài)w0轉(zhuǎn)移到狀態(tài)w1，將該行為標(biāo)簽記為［rq_0］。如果0＜i＜K，則將以速率λ 從狀態(tài)wi轉(zhuǎn)移到狀態(tài)wi+1，將該行為標(biāo)簽記為［rq］。如果i=K，即等待隊(duì)列已滿(mǎn)，新請(qǐng)求將被拒絕，則存在一個(gè)轉(zhuǎn)移速率為λ，到狀態(tài)wK自身的轉(zhuǎn)移，將該行為標(biāo)簽記為［lose］。

當(dāng)配置器完成當(dāng)前任務(wù)，將完成配置任務(wù)的行為標(biāo)簽記為［dp］。等待隊(duì)列模塊將在［dp］上發(fā)生被動(dòng)轉(zhuǎn)移，故轉(zhuǎn)移速率為1。如果等待隊(duì)列中當(dāng)前請(qǐng)求數(shù)大于0，應(yīng)先進(jìn)行配置決策。只有請(qǐng)求滿(mǎn)足決策條件才能進(jìn)入配置階段，模塊狀態(tài)從wi轉(zhuǎn)移至狀態(tài)wi-1；否則請(qǐng)求將繼續(xù)等待，即發(fā)生一個(gè)到狀態(tài)wi自身的轉(zhuǎn)移。等待隊(duì)列模塊的狀態(tài)轉(zhuǎn)移過(guò)程如圖4所示。

圖4 等待隊(duì)列模塊的狀態(tài)轉(zhuǎn)移過(guò)程Fig.4 State transition process of queuing module

2.2.2 配置器模塊

配置器對(duì)待處理的請(qǐng)求進(jìn)行配置決策，并對(duì)滿(mǎn)足決策條件的請(qǐng)求分配所需的容器資源。當(dāng)配置器與等待隊(duì)列中都沒(méi)有請(qǐng)求需要處理時(shí)，配置模塊處在空閑狀態(tài)，如果當(dāng)前有新請(qǐng)求到達(dá)且滿(mǎn)足決策條件，則配置器為其分配及部署容器，狀態(tài)進(jìn)入工作狀態(tài)；否則配置器需要在有請(qǐng)求執(zhí)行完成并釋放占用的容器資源時(shí)，反復(fù)進(jìn)行決策，直至決策條件滿(mǎn)足，該狀態(tài)稱(chēng)為決策狀態(tài)。以d0表示空閑狀態(tài)，d1表示決策狀態(tài)，d2表示工作狀態(tài)。設(shè)配置器模塊的狀態(tài)集為S=｛d0，d1，d2｝，顯然，當(dāng)新的請(qǐng)求達(dá)到、配置器完成當(dāng)前請(qǐng)求的配置或者有服務(wù)執(zhí)行完成時(shí)，都可能引起配置器模塊的狀態(tài)變化。下面具體描述其狀態(tài)轉(zhuǎn)移過(guò)程。

當(dāng)新請(qǐng)求到達(dá)且等待隊(duì)列為空時(shí)，配置器模塊將在行為標(biāo)簽［rq_0］上發(fā)生被動(dòng)轉(zhuǎn)移，轉(zhuǎn)移速率為1。若當(dāng)前狀態(tài)為不為d0，則發(fā)生一個(gè)到狀態(tài)本身的轉(zhuǎn)移；若當(dāng)前狀態(tài)為d0，即配置器處在空閑狀態(tài)，則應(yīng)先對(duì)到達(dá)的服務(wù)請(qǐng)求進(jìn)行配置決策，如果滿(mǎn)足決策條件，狀態(tài)轉(zhuǎn)移至d2，否則狀態(tài)轉(zhuǎn)移至d1。

設(shè)配置器執(zhí)行速率為γ。當(dāng)前配置任務(wù)完成時(shí)，如果此時(shí)還有請(qǐng)求等待且滿(mǎn)足決策條件，則請(qǐng)求進(jìn)入配置階段，發(fā)生一個(gè)到狀態(tài)本身的轉(zhuǎn)移，否則請(qǐng)求需繼續(xù)等待，狀態(tài)轉(zhuǎn)移到d1。如果等待隊(duì)列為空，則狀態(tài)轉(zhuǎn)移到d2。將該行為標(biāo)簽記為［dp］。

當(dāng)虛擬機(jī)模塊中有服務(wù)執(zhí)行完成時(shí)，執(zhí)行完成的請(qǐng)求釋放占用的資源，將該行為標(biāo)簽記為［sv］。配置器模塊將在行為標(biāo)簽［sv］上發(fā)生被動(dòng)轉(zhuǎn)移，轉(zhuǎn)移速率為1。如果此時(shí)狀態(tài)為d1且滿(mǎn)足決策條件，則待配置的請(qǐng)求可進(jìn)入配置階段，狀態(tài)轉(zhuǎn)移到d2，否則發(fā)生一個(gè)到狀態(tài)本身d1的轉(zhuǎn)移。

配置器模塊的狀態(tài)轉(zhuǎn)移過(guò)程如圖5所示。

圖5 配置器模塊的狀態(tài)轉(zhuǎn)移過(guò)程Fig.5 State transition process of configulator module

2.2.3 虛擬機(jī)模塊

服務(wù)請(qǐng)求配置完成之后，將在虛擬機(jī)中進(jìn)行服務(wù)的部署、啟動(dòng)與執(zhí)行。虛擬機(jī)模塊的狀態(tài)可以用一個(gè)二元組V=（r，m）來(lái)描述，其中，r表示正在執(zhí)行中的服務(wù)請(qǐng)求數(shù)，m 表示剩余可部署的容器數(shù)。當(dāng)需要x 個(gè)容器的服務(wù)請(qǐng)求配置完成，虛擬機(jī)中剩余可部署的容器數(shù)將減少x，正在執(zhí)行中的服務(wù)請(qǐng)求數(shù)加1。當(dāng)服務(wù)請(qǐng)求執(zhí)行完成，將會(huì)釋放占用的容器資源并離開(kāi)系統(tǒng)，剩余可部署的容器數(shù)將增加x，正在執(zhí)行中的服務(wù)請(qǐng)求減1。設(shè)虛擬機(jī)中最多可部署容器個(gè)數(shù)為N，當(dāng)前狀態(tài)為（i，j），當(dāng)前配置任務(wù)完成或有服務(wù)執(zhí)行完成時(shí)，都將會(huì)引起狀態(tài)變化。下面具體描述其狀態(tài)轉(zhuǎn)移過(guò)程。

當(dāng)有服務(wù)執(zhí)行完成時(shí)，設(shè)執(zhí)行請(qǐng)求花費(fèi)的時(shí)間服從參數(shù)為μ 的負(fù)指數(shù)分布，如果執(zhí)行完成的請(qǐng)求類(lèi)型為x，則系統(tǒng)狀態(tài)以速率μ轉(zhuǎn)移到（i -1，j+x），該行為標(biāo)簽記為［sv］。

當(dāng)前配置任務(wù)完成時(shí)，虛擬機(jī)模塊將在行為標(biāo)簽［dp］上發(fā)生被動(dòng)轉(zhuǎn)移，轉(zhuǎn)移速率為1，狀態(tài)轉(zhuǎn)移到（i+1，j-x）。

虛擬機(jī)模塊的狀態(tài)轉(zhuǎn)移過(guò)程如圖6所示。

圖6 虛擬機(jī)模塊的狀態(tài)轉(zhuǎn)移過(guò)程Fig.6 State transition process of virtual machine module

3 連續(xù)隨機(jī)邏輯語(yǔ)法和語(yǔ)義

第2 章已經(jīng)構(gòu)造出微服務(wù)平臺(tái)中各個(gè)組件運(yùn)行過(guò)程的概率模型，還需要借助時(shí)序邏輯公式來(lái)嚴(yán)謹(jǐn)?shù)乜坍?huà)待驗(yàn)證的性質(zhì)［14］，其中連續(xù)隨機(jī)邏輯公式（Continuous Stochastic Logic，CSL）能夠描述CTMC 模型中的時(shí)間連續(xù)性和概率特征，故采用CSL對(duì)待驗(yàn)證的屬性進(jìn)行描述。本文將增加了獎(jiǎng)勵(lì)回報(bào)的CSL 命名為連續(xù)隨機(jī)回報(bào)邏輯公式（Continuous Stochastic Reward Logic，CSRL）［15］，首先給出CSRL的語(yǔ)法定義。

定義3CSRL 語(yǔ)法。設(shè)φ 為連續(xù)時(shí)間Markov 鏈上的狀態(tài)公式，φ 為路徑公式，則Markov 鏈模型上的狀態(tài)公式、路徑公式可分別定義為：

式中：a ∈AP 為原子命題，?∈{＞，＜，≥，≤}，p∈［0，1］，I 與J為非負(fù)實(shí)區(qū)間，I表示某個(gè)時(shí)間間隔，J表示時(shí)間間隔內(nèi)累積回報(bào)值的區(qū)間，?p 用于限定概率范圍為瞬時(shí)概率算子為穩(wěn)態(tài)概率算子，操作符X和U 是標(biāo)準(zhǔn)的時(shí)序邏輯操作符，用于刻畫(huà)Markov鏈中的路徑應(yīng)該滿(mǎn)足的性質(zhì)，其中X代表“下一個(gè)”，U 代表“直到”。為了在Markov 鏈模型中對(duì)相關(guān)的CSRL 性質(zhì)進(jìn)行推理，必須給出CSRL 邏輯公式可滿(mǎn)足語(yǔ)義的定義。

定義4CSRL 語(yǔ)義。定義一個(gè)LMRM 為M=（S，sinit，L，R，RoS，RoT），在CSRL 公式中，若其中狀態(tài)s滿(mǎn)足狀態(tài)公式φ，則表示為M，s ?φ。CSRL狀態(tài)公式可滿(mǎn)足語(yǔ)義定義如下：

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

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

4 實(shí)驗(yàn)及結(jié)果分析

為了驗(yàn)證上述方法的可適用性，本章將對(duì)一個(gè)微服務(wù)組合平臺(tái)的資源配置過(guò)程進(jìn)行建模分析，并設(shè)計(jì)了3 個(gè)實(shí)驗(yàn)：實(shí)驗(yàn)1 以虛擬機(jī)中的容器總數(shù)為變量參數(shù)，驗(yàn)證在不同容器總數(shù)下，等待隊(duì)列的平均長(zhǎng)度，并檢測(cè)方法可支持的數(shù)據(jù)規(guī)模；實(shí)驗(yàn)2 通過(guò)改變運(yùn)行的時(shí)間區(qū)間大小，來(lái)研究運(yùn)行時(shí)間長(zhǎng)短對(duì)驗(yàn)證效率及驗(yàn)證結(jié)果的影響；實(shí)驗(yàn)3 通過(guò)對(duì)更為復(fù)雜的請(qǐng)求丟失率、虛擬機(jī)資源利用率等性質(zhì)進(jìn)行驗(yàn)證，進(jìn)一步說(shuō)明方法的可適用性。

4.1 實(shí)驗(yàn)配置及參數(shù)

本文實(shí)驗(yàn)的運(yùn)行環(huán)境為Windows 10 系統(tǒng)，Intel Core i7-7700 CPU 3.60 GHz 處理器，16.0 GB 內(nèi)存，實(shí)驗(yàn)工具為概率模型檢測(cè)器PRISM，版本號(hào)為4.5。

本文以基于微服務(wù)的在線購(gòu)物平臺(tái)作為研究對(duì)象，將資源配置過(guò)程抽象出來(lái)建模成LMRM 模型，并通過(guò)檢測(cè)工具PRISM 對(duì)期望檢驗(yàn)的性質(zhì)進(jìn)行實(shí)驗(yàn)分析。在線購(gòu)物平臺(tái)包含4 個(gè)主要的服務(wù)功能：商品服務(wù)、購(gòu)物車(chē)服務(wù)、訂單服務(wù)和個(gè)人中心服務(wù)。假設(shè)在該場(chǎng)景下的商品服務(wù)由3 個(gè)子微服務(wù)組合完成，且被調(diào)用的概率占所有服務(wù)請(qǐng)求的1/2；購(gòu)物車(chē)服務(wù)由4 個(gè)子微服務(wù)組合完成，且被調(diào)用的概率占所有服務(wù)請(qǐng)求的1/4；訂單服務(wù)由5 個(gè)子微服務(wù)組合完成，且被調(diào)用的概率占所有服務(wù)請(qǐng)求的3/16；個(gè)人信息服務(wù)由4 個(gè)子微服務(wù)組合完成，且被調(diào)用的概率占所有服務(wù)請(qǐng)求的1/16。表2列出了各服務(wù)功能的基本參數(shù)。

表2 不同類(lèi)型的服務(wù)參數(shù)Tab.2 Different types of service parameters

實(shí)驗(yàn)中請(qǐng)求數(shù)量、請(qǐng)求處理速率及虛擬機(jī)規(guī)模等常量的取值參考了文獻(xiàn)［8］，將本文實(shí)驗(yàn)得到的驗(yàn)證結(jié)果與通過(guò)文獻(xiàn)［8］中建模與驗(yàn)證方法獲得的實(shí)驗(yàn)結(jié)果做對(duì)比，可進(jìn)一步證明方法的可靠性。

4.2 實(shí)驗(yàn)1

模型檢測(cè)的原理是對(duì)模型的狀態(tài)空間進(jìn)行遍歷搜索，因此具有自動(dòng)化程度高、保證驗(yàn)證結(jié)果正確等優(yōu)點(diǎn)，然而隨著系統(tǒng)規(guī)模的擴(kuò)大，其狀態(tài)數(shù)會(huì)呈指數(shù)增長(zhǎng)，容易產(chǎn)生狀態(tài)爆炸的問(wèn)題。為了確保實(shí)驗(yàn)的順利進(jìn)行，首先需要對(duì)模型可支持的數(shù)據(jù)規(guī)模進(jìn)行檢測(cè)。實(shí)驗(yàn)1 以虛擬機(jī)中一共能部署的容器數(shù)量N 為變量，對(duì)不同N 取值下的模型狀態(tài)數(shù)、轉(zhuǎn)移數(shù)及驗(yàn)證耗費(fèi)的時(shí)長(zhǎng)等進(jìn)行檢測(cè)，以驗(yàn)證模型可支持的數(shù)據(jù)規(guī)模。

將等待隊(duì)列長(zhǎng)度的獎(jiǎng)勵(lì)回報(bào)函數(shù)標(biāo)簽記為“queue_size”，從0時(shí)刻開(kāi)始的T個(gè)單位時(shí)間內(nèi)，系統(tǒng)的平均等待隊(duì)列長(zhǎng)度的CSRL描述如式（12）：

設(shè)等待隊(duì)列一共能接受的請(qǐng)求個(gè)數(shù)K 為10，請(qǐng)求到達(dá)速率λ 的數(shù)值為8，請(qǐng)求配置速率γ 的數(shù)值為10，微服務(wù)執(zhí)行完成速率μ 的數(shù)值為3。將變量N 在30～70 每隔10 取一點(diǎn)作為參數(shù)，測(cè)試在T=100 個(gè)單位時(shí)間內(nèi)等待隊(duì)列的平均長(zhǎng)度。驗(yàn)證花費(fèi)的時(shí)間取決于實(shí)驗(yàn)設(shè)備的數(shù)據(jù)處理能力，在本文實(shí)驗(yàn)環(huán)境下驗(yàn)證結(jié)果及模型的狀態(tài)數(shù)、轉(zhuǎn)移數(shù)和驗(yàn)證所花費(fèi)的時(shí)長(zhǎng)記錄如表3。

表3 實(shí)驗(yàn)1驗(yàn)證結(jié)果Tab.3 Verification results of experiment 1

由表3 可知，隨著虛擬機(jī)內(nèi)可部署容器數(shù)量的增加等待隊(duì)列的平均長(zhǎng)度逐漸變短，與實(shí)際運(yùn)行情況相符，說(shuō)明了本文方法的可行性；且系統(tǒng)狀態(tài)數(shù)隨著容器數(shù)量的增加而增加，當(dāng)N 為70 時(shí)，驗(yàn)證用時(shí)才有大幅度的增加。N 為90 時(shí)，雖然驗(yàn)證已需要花費(fèi)較高的時(shí)間成本，但依然能夠給出準(zhǔn)確的驗(yàn)證結(jié)果，說(shuō)明本文方法可用于狀態(tài)數(shù)較多的模型驗(yàn)證。

4.3 實(shí)驗(yàn)2

實(shí)驗(yàn)2 在實(shí)驗(yàn)1 的基礎(chǔ)上，對(duì)更為復(fù)雜的系統(tǒng)性能指標(biāo)：虛擬機(jī)中資源的利用率進(jìn)行驗(yàn)證。設(shè)資源利用率的獎(jiǎng)勵(lì)回報(bào)函數(shù)標(biāo)簽記為“utilization”，從0時(shí)刻開(kāi)始的T個(gè)單位時(shí)間內(nèi)虛擬機(jī)中容器資源的利用率的CSRL描述如式（13）：

實(shí)驗(yàn)2 以N 為變量，在40～80 每隔10 取一點(diǎn)作為變量N的參數(shù)進(jìn)行測(cè)試，常量取值與實(shí)驗(yàn)1 相同。在對(duì)不同N 的取值進(jìn)行實(shí)驗(yàn)時(shí)，從數(shù)值0～100 內(nèi)每隔10 個(gè)單位時(shí)間取一點(diǎn)為參數(shù)進(jìn)行驗(yàn)證，以模擬虛擬機(jī)中資源利用率隨系統(tǒng)運(yùn)行的變化。PRISM 可根據(jù)設(shè)定參數(shù)自動(dòng)生成驗(yàn)證結(jié)果的折線圖如圖7所示。

圖7 實(shí)驗(yàn)2驗(yàn)證結(jié)果Fig.7 Verification results of experiment 2

由圖7 可知，在不同的虛擬機(jī)容量下，資源利用率隨著系統(tǒng)運(yùn)行時(shí)間的增加而發(fā)生的變化。虛擬機(jī)的容量越小，資源利用率就越高，且在越小的容量下，資源利用率隨運(yùn)行時(shí)間變化增加的幅度就越大。到100 個(gè)時(shí)間單位時(shí)變化幅度基本趨于穩(wěn)定，即運(yùn)行中的微服務(wù)組合平臺(tái)的資源利用率一般維持在0.9 左右，變化曲線與現(xiàn)有研究中的實(shí)驗(yàn)結(jié)果相似，且與實(shí)際運(yùn)行情況相符。

4.4 實(shí)驗(yàn)3

對(duì)虛擬機(jī)資源利用率的驗(yàn)證只涉及一個(gè)獎(jiǎng)勵(lì)回報(bào)函數(shù)“utilization”，而驗(yàn)證另外一些性能指標(biāo)時(shí)可能涉及多個(gè)獎(jiǎng)勵(lì)回報(bào)函數(shù)。如驗(yàn)證一個(gè)時(shí)間間隔內(nèi)服務(wù)請(qǐng)求的拒絕率，需要涉及被拒絕的服務(wù)請(qǐng)求數(shù)和服務(wù)請(qǐng)求總數(shù)兩個(gè)獎(jiǎng)勵(lì)回報(bào)函數(shù)。將被拒絕的服務(wù)請(qǐng)求數(shù)的獎(jiǎng)勵(lì)回報(bào)函數(shù)標(biāo)簽記為“l(fā)ose”，服務(wù)請(qǐng)求總數(shù)的獎(jiǎng)勵(lì)回報(bào)函數(shù)標(biāo)簽記為“quest”，從0 時(shí)刻開(kāi)始的T個(gè)單位時(shí)間內(nèi)的請(qǐng)求拒絕率用CSRL描述如式（14）：

實(shí)驗(yàn)3 以N 為變量，在40～80 每隔10 取一點(diǎn)作為變量N的參數(shù)進(jìn)行測(cè)試，常量取值與實(shí)驗(yàn)1 相同。在對(duì)不同N 的取值進(jìn)行實(shí)驗(yàn)時(shí)，從數(shù)值0～200 內(nèi)每隔10 個(gè)單位時(shí)間取一點(diǎn)為參數(shù)進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如圖8所示。

由圖8 可知，隨著虛擬機(jī)的容量增大，服務(wù)被拒絕的概率降低，且請(qǐng)求拒絕率在系統(tǒng)運(yùn)行一段時(shí)間之后逐漸趨于穩(wěn)定，請(qǐng)求拒絕率的變化曲線與文獻(xiàn)［8］中的變化曲線相似，且與實(shí)際運(yùn)行情況相符。

圖8 實(shí)驗(yàn)3驗(yàn)證結(jié)果Fig.8 Verification results of experiment 3

5 結(jié)語(yǔ)

本文提出一種基于概率模型檢測(cè)的微服務(wù)組合平臺(tái)性能評(píng)估方法。首先，對(duì)微服務(wù)平臺(tái)中的服務(wù)組合及資源配置過(guò)程進(jìn)行描述，并將整體系統(tǒng)拆分為三個(gè)子模塊：等待隊(duì)列模塊、配置器模塊、虛擬機(jī)模塊，采用概率模型LMRM 對(duì)三個(gè)子模塊分別進(jìn)行建模；接著，用概率邏輯公式CSRL 對(duì)待測(cè)性質(zhì)進(jìn)行刻畫(huà)；最后，設(shè)計(jì)一個(gè)在線購(gòu)物平臺(tái)的實(shí)例，使用檢測(cè)工具PRISM 對(duì)平臺(tái)性能進(jìn)行模擬驗(yàn)證，驗(yàn)證了方法可支持的數(shù)據(jù)規(guī)模、對(duì)復(fù)雜性質(zhì)進(jìn)行驗(yàn)證的可行性等，以證明方法的可行性。下一步工作將考慮更加復(fù)雜的請(qǐng)求調(diào)度情形，同時(shí)進(jìn)一步簡(jiǎn)化模型以減少系統(tǒng)狀態(tài)數(shù)量。