自適應軟件動態(tài)過程時間特性建模與驗證方法

韓德帥，邢建春，楊啟亮,2，李決龍

(1.陸軍工程大學 國防工程學院，南京 210007； 2.清華大學 土木工程系，北京 100084;3.海軍海防工程研究中心，北京 100841)

0 引言

自適應軟件(self-adaptive software)能夠在運行時實時監(jiān)測上下文變化并對自身進行動態(tài)調(diào)整，以消除或減輕變化帶來的不利影響。它能夠有效應對運行環(huán)境和用戶需求的頻繁變化，降低軟件維護壓力，增強自身容錯和應對變化的能力，現(xiàn)已成為軟件工程領域的熱點研究問題[1-4]。

為提高自適應軟件的可靠性，需對自適應軟件的動態(tài)過程進行形式化建模和分析?；诖?，國內(nèi)外學者針對自適應軟件的形式化方法開展了大量研究[5-7]，能夠較好地支持自適應邏輯和自適應行為的刻畫和分析，卻鮮有研究考慮自適應動態(tài)過程的時間約束。然而，實踐表明，在時間攸關(guān)應用領域，自適應軟件系統(tǒng)能否正確運行，不僅依賴于自適應邏輯的正確性，而且要考慮系統(tǒng)自適應過程的時間特性。首先，自適應軟件的開發(fā)需在原應用邏輯之上構(gòu)建自適應邏輯，而自適應邏輯的引入勢必會給原系統(tǒng)帶來時間開銷，將自適應邏輯的時間開銷降到最低需綜合考慮自適應各個子過程(如監(jiān)控、分析、規(guī)劃和執(zhí)行等)的時間約束；其次，自適應軟件的很多應用場景具有及時響應性，如課題組前期研究中的自適應火災應急響應系統(tǒng)[8]，需要系統(tǒng)能夠及時捕獲險情、及時傳遞險情并能夠及時啟動應急設備，要刻畫這類具有實時性的自適應場景，時間特性是一個重要方面；最后，軟件形式化方法只能分析和驗證自適應邏輯的正確性，不能衡量自適應邏輯的響應速度和響應效果，現(xiàn)有研究尚缺乏性能指標和評估方法以全面評估自適應邏輯的性能。

基于此，本文提出一種自適應軟件動態(tài)過程時間特性建模與驗證方法。首先，本文顯式定義了監(jiān)控周期、延遲觸發(fā)時間、自適應過程截止時間等時間特性用以刻畫自適應動態(tài)過程各子過程的時間約束，并定義了自適應調(diào)節(jié)時間和自適應穩(wěn)定時間用以定量評估自適應邏輯的響應速度和響應效果；更進一步地，本文基于時間自動機網(wǎng)絡構(gòu)建了自適應軟件動態(tài)過程時間特性建模模板，實現(xiàn)了自適應軟件時間特性的顯式刻畫和建模方法的復用；最后，本文將自適應軟件時間特性描述為定時計算樹邏輯(Timed Computation Tree Logic, TCTL)形式，并借助模型檢驗工具UPPAAL進行自適應軟件時間特性分析和驗證。

1 相關(guān)工作

軟件自適應已成為軟件工程領域所關(guān)注的一個焦點問題，從IBM的自治計算(autonomic computing)[9]、美國軍方的DASADA(Dynamic Assembly for System Adaptability, Dependability and Assurance)計劃、每年國際軟件工程大會ICSE(International Conference on Software Engineering)的SEAMS(symposia on Software Engineering for Adaptive and self-Managing Systems)研討會、《軟件學報》自適應軟件?？戎卸伎煽闯鲕浖赃m應問題研究的重要性，其中針對自適應軟件的形式化建模方法的研究也吸引了眾多研究學者。

課題組在前期工作中提出一種UML與時間自動機相結(jié)合的自適應軟件建模方法[7]，汲取了UML直觀易理解和時間自動機嚴謹無二義性的優(yōu)點，實現(xiàn)了自適應軟件結(jié)構(gòu)特征和行為特性的顯式刻畫和形式化驗證。Ramirez等[10]提出了基于UML的設計模式，de la Iglesia等[5]總結(jié)并提煉出一套自適應軟件形式化模板(formal templates)，實現(xiàn)了自適應軟件形式化模型的復用，降低了其形式化建模難度。此外，不少學者還探索使用進程代數(shù)CSP(Communicating Sequential Process)[11]、 Markov 模型[12]、 Petri網(wǎng)[13]等其他形式化工具進行軟件自適應的形式化建模和分析，Weyns 等[14]作了較為詳細的綜述， 在此不再贅述。

上述這些研究的關(guān)注點集中在自適應邏輯的形式化描述與分析，其能夠較好地刻畫自適應過程的行為特性，并進行形式化分析和驗證；然而，上述研究均未提供自適應軟件動態(tài)過程時間特性的刻畫與分析方法。實現(xiàn)自適應軟件動態(tài)過程時間特性的顯式定義和形式化描述是本文研究的動機。

Camilli等[15]提出一種基礎時間Petri網(wǎng)(Time-Basic Petri nets)用于自適應軟件各過程截止時間(deadline)和時間間隔(time interval)的刻畫，實現(xiàn)了對時間攸關(guān)(time-critical)自適應系統(tǒng)的形式化建模與驗證。Hachicha等[16]提出面向自適應軟件的延遲時間(delay time)和逾期時間(expiry time)等時序性質(zhì)，并提出通過擴展Event-B[17]模型形式刻畫上述性質(zhì)。上述研究開始關(guān)注自適應軟件時間特性的刻畫，對本文研究產(chǎn)生一定啟發(fā)。同上述研究相比，本文更為系統(tǒng)地定義了自適應軟件動態(tài)過程的時間特性，增加了自適應調(diào)節(jié)時間和自適應穩(wěn)定時間等性能指標來定量評估自適應邏輯，本文還提供了一種基于時間自動機網(wǎng)絡的自適應軟件時間特性建模模板，實現(xiàn)建模方法的復用，降低自適應軟件時間特性的刻畫難度。

此外，Calinescu等[12]、Filieri等[18]和Ghezzi等[19]還考慮了自適應軟件中時間特性的不確定性，提出將時間特性作為一種非功能需求(non-functional requirement)進行分析，利用概率模型檢驗(probabilistic model checking)的方法分析了響應時間(response time)等時間特性。同上述研究相比，本文側(cè)重面向時間攸關(guān)領域(time-critical)的自適應軟件時間特性的顯式定義、形式化建模和分析驗證。除響應時間(在本文為自適應調(diào)節(jié)時間)外，本文還較為系統(tǒng)地定義了延遲觸發(fā)時間、截止時間等時間特性。

2 自適應軟件時間特性定義

2.1 自適應軟件MAPE-K模型

IBM 提出的MAPE-K[20]自治計算模型已廣泛應用于自適應軟件的設計中，它將自適應軟件系統(tǒng)分為自適應邏輯和應用邏輯兩部分。自適應邏輯由監(jiān)控(Monitor)、分析(Analyze)、規(guī)劃(Plan)和執(zhí)行(Execute)四個模塊外加一個知識庫(Knowledge)模塊構(gòu)成，其中：監(jiān)控模塊用于從應用邏輯抽取屬性或狀態(tài)信息；分析模塊用于判定系統(tǒng)中的錯誤和異常，如某一系統(tǒng)屬性是否越限等；規(guī)劃模塊主要側(cè)重于當發(fā)現(xiàn)系統(tǒng)出現(xiàn)問題時決定采用何種動作；執(zhí)行模塊關(guān)注于執(zhí)行規(guī)劃階段所選擇的自適應動作，對軟件自身施加影響以應對變化；知識庫模塊存儲系統(tǒng)自適應策略、歷史數(shù)據(jù)等。如圖1所示。

圖1 MAPE-K自適應軟件模型 Fig. 1 MAPE-K self-adaptive software model

MAPE-K模型定義了自適應軟件的結(jié)構(gòu)組成和自適應動態(tài)過程。然而，自適應軟件能否正確運行，不僅要考慮自適應動態(tài)過程中各子過程行為的正確性，而且要考慮各子過程的時間特性，本文將以MAPE-K自適應模型為基礎，定義和刻畫自適應軟件動態(tài)過程的時間特性。

2.2 典型自適應場景

SUIS(Ship sUpplying Information System)[21]是一個基于服務(Web-service)的艦船保障信息系統(tǒng)，其以服務的形式實時處理艦船提交的保障需求。在出航任務密集時期，SUIS要在短時間內(nèi)處理大量的保障需求，為保證系統(tǒng)能夠及時響應服務請求，SUIS以云架構(gòu)(cloud-based architecture)的形式來實現(xiàn)，并構(gòu)建自適應邏輯以動態(tài)監(jiān)測和調(diào)整云端資源(計算節(jié)點和存儲節(jié)點)，滿足動態(tài)變化的用戶需求，系統(tǒng)整體架構(gòu)如圖2所示。

圖2 基于云架構(gòu)的艦船保障自適應信息系統(tǒng) Fig. 2 Self-adaptive ship supplying information system based on cloud computing architecture

為提高服務保障的快速性和準確性，自適應邏輯需周期性監(jiān)測云端服務器的CPU利用率(CPU Utilization)，并根據(jù)CPU利用率的變化動態(tài)調(diào)整服務器池中服務器的數(shù)量(ServerNumber)；此外，還需對自適應決策的每個子過程(MAPE的各個過程)進行時間約束，以提高云端響應的準確性。例如，自適應策略“ifUtilization>MforNseconds, then addPmore VMs”定義如果服務器CPU利用率在N秒內(nèi)都超過上限值M，則添加P臺虛擬機(Virtual Machine, VM)，該策略在分析(Analyze)階段添加延時觸發(fā)時間約束N，能夠提高監(jiān)測的準確性。此外，該案例還需刻畫監(jiān)測周期、自適應動態(tài)過程的截止時間、自適應調(diào)節(jié)時間等時間約束，將在下文結(jié)合案例詳細闡述。

2.3 自適應軟件時間特性分析與定義

自適應軟件時間特性用以約束自適應軟件動態(tài)過程(如監(jiān)控、分析、規(guī)劃和動作等)的時間特性。如圖3所示，自適應邏輯需定期監(jiān)測軟件上下文狀態(tài)并依此決定是否啟動自適應過程，為此，在軟件自適應的監(jiān)控階段定義監(jiān)控周期MPeriod，使其周期性抽取軟件上下文狀態(tài)信息(如2.2節(jié)自適應場景中CPU利用率Utilization)，并觸發(fā)后續(xù)自適應過程；在分析階段定義延遲觸發(fā)時間ADelay，在監(jiān)控變量發(fā)生越限行為(如案例中Utilization>M)時，再持續(xù)監(jiān)測ADelay時間(如案例中Nseconds)，若監(jiān)測變量仍然越限則觸發(fā)后續(xù)自適應過程，定義延遲觸發(fā)時間可以提高監(jiān)測準確性；由于自適應規(guī)劃和執(zhí)行階段需進行較為復雜的計算，在此定義截止時間PDeadline和EDeadline來限制自適應邏輯的時間開銷，各時間特性定義如表1所示。

圖3 自適應軟件動態(tài)過程時間特性示意 Fig. 3 Temporal properties of self-adaptive software dynamic processes

如圖4所示，自適應軟件在面臨變化時會作出響應以及時消除或減輕變化帶來的不利影響，最終使系統(tǒng)恢復穩(wěn)定狀態(tài)。然而，如何評價自適應響應的及時性以及自適應響應帶來的效果，現(xiàn)有研究尚缺乏相應的衡量指標。為此，本文定義了自適應調(diào)節(jié)時間TAdjust和自適應穩(wěn)定時間TSteady，如表1所示，TAdjust表征系統(tǒng)在遭遇變化后恢復正常狀態(tài)的快速性，TSteady表征系統(tǒng)遭遇變化后恢復穩(wěn)定狀態(tài)的快速性。自適應軟件開發(fā)人員可根據(jù)實際需求不斷優(yōu)化軟件自適應策略，使系統(tǒng)的自適應調(diào)節(jié)時間和自適應穩(wěn)定時間降到最低。

表1 自適應軟件動態(tài)過程時間特性定義Tab. 1 Definitions of temporal properties of self-adaptive software dynamic processes

圖4 自適應調(diào)節(jié)時間和穩(wěn)定時間示意 Fig. 4 Self-adaptive adjusting time and steady time

3 自適應軟件動態(tài)過程時間特性建模

時間自動機模型在自適應系統(tǒng)形式化建模領域取得了良好的應用效果，然而，現(xiàn)有研究鮮有考慮自適應軟件的時間特性。為此，本文在現(xiàn)有研究基礎上構(gòu)建了基于時間自動機的自適應軟件動態(tài)過程時間特性建模模板，實現(xiàn)自適應軟件時間特性的顯式刻畫和形式化模型的復用。

3.1 時間自動機模型

時間自動機模型(timed automata)[22]對傳統(tǒng)有限自動機模型進行了擴展，加入了時間約束，以支持對系統(tǒng)實時特性的描述和形式化分析，其可定義為一個六元組：TA〈L,l0,S,A,E,I〉。其中：L是有限位置的集合，L?Location；l0∈L表示初始位置initiallocation；S是邊E上約束的集合，S?Guard；A是所有動作的集合，包括輸入、輸出和內(nèi)部三類動作，A={a!|a∈Chan}∪{a?|a∈Chan}∪{τ}；E是有向邊的集合,E?L×A×G(c,v)×U(c,v)×L, (l,a,g,u,l′)表示從位置l到位置l′ 的遷移，遷移過程伴有衛(wèi)式約束g、賦值操作u和動作a；I是不變式invariant的集合；I?Guard用以約束位置的狀態(tài)。

由多個并發(fā)時間自動機模型可組成一個時間自動機網(wǎng)絡模型(Timed Automata Network, TAN)，記為：TAN≡TA1‖TA2‖…‖TAn。

模型檢驗工具UPPAAL[23]采用時間自動機網(wǎng)絡模擬實時系統(tǒng)的行為，采用時序邏輯(Timed Computation Tree Logic, TCTL)刻畫系統(tǒng)的性質(zhì)，并對系統(tǒng)進行自動化分析和驗證。

3.2 自適應軟件動態(tài)過程時間特性建模模板

自適應軟件的形式化建模難度大、耗時長，其行為特性較難刻畫。為此，本節(jié)基于時間自動機網(wǎng)絡構(gòu)建了自適應軟件動態(tài)過程時間特性建模模板，以顯式刻畫自適應軟件的動態(tài)行為及時間特性，實現(xiàn)自適應軟件形式化模型的復用，如圖5所示。本文用時間自動機模型刻畫“Monitor-Analyze-Plan-Execute”自適應軟件動態(tài)過程，用“聲明(declaration)”刻畫“知識庫(Knowledge)”，用時鐘clock、衛(wèi)式guard和不變式invariant刻畫自適應軟件的時間特性。

具體而言，監(jiān)控Monitor模板如圖5(a)所示，其將Monitor分為“定時-數(shù)據(jù)獲取-比較-觸發(fā)”四個階段，在定時階段通過guard和invariant組合定義監(jiān)控周期T=Period；在數(shù)據(jù)獲取階段，通過getData()函數(shù)獲取監(jiān)控數(shù)據(jù)；在“比較”階段通過將監(jiān)控數(shù)據(jù)和設定的上下限比較，確定監(jiān)控數(shù)據(jù)低于下限狀態(tài)“l(fā)ow”或高于上限狀態(tài)“high”或處于上下限之間“NoChange”，并根據(jù)不同狀態(tài)觸發(fā)不同分析標志flagA=-1,flagA=1或flagA=0。

分析Analyze模板如圖5(b)所示，其由flagA觸發(fā)，分為“延時-比較-觸發(fā)”三個階段，在延時階段定義延遲觸發(fā)時間T1=Delay1和T2=Delay2，若在延遲時間內(nèi)監(jiān)控數(shù)據(jù)保持越限狀態(tài)，則判定系統(tǒng)處于資源“過滿足OverSatisfied”或“不滿足UnderSatisfied”狀態(tài)，并觸發(fā)相應的規(guī)劃標志flagP。

規(guī)劃Plan模板如圖5(c)所示，其由flagP觸發(fā)，在該模板中定義了截止時間T<=D，用來限制規(guī)劃函數(shù)add()和remove()的時間開銷。類似地，本文定義了執(zhí)行Execute模板和應用邏輯Application模板，及相應的截止時間模板，如圖5(d)和5(e)所示。

此外，為模擬軟件上下文變化帶來的影響，本文定義了上下文變化Dynamics模板，其能夠周期性地產(chǎn)生一個位于[-m,m]的隨機量，用以模擬環(huán)境干擾，如圖5(f)所示。本文在自動機的聲明declaration中構(gòu)造了知識庫Knowledge模板，用來定義自適應過程的相關(guān)變量和函數(shù)，如圖5(g)所示。在Knowledge中還定義了全局時鐘變量t，它能夠記錄監(jiān)控變量發(fā)生變化的各個時刻，為后續(xù)自適應調(diào)節(jié)時間TAdjust和自適應穩(wěn)定時間TSteady的分析作準備。

4 自適應軟件時間特性分析與驗證

在前期研究[7]中，課題組針對自適應軟件有無死鎖、自適應動作有效性等性質(zhì)進行了形式化描述和驗證，下文將在3.2節(jié)建立的形式化模板基礎上，用定時計算樹邏輯(TCTL)刻畫自適應軟件的延遲觸發(fā)時間和截止時間等時間特性，并借助時間自動機UPPAAL進行驗證。

4.1 自適應軟件延遲觸發(fā)時間驗證

以圖5(b)為例，該延遲觸發(fā)時間特性可描述為“如果函數(shù)compare()在延遲時間Delay1結(jié)束后仍然等于-1，則變遷analyze1到OverSatisfied發(fā)生”。上述性質(zhì)成立需同時滿足兩個條件：1) 若變遷從analyze1到OverSatisfied發(fā)生，則T1>=Delay1；2) 當T1

Analyze.analyze1-->Analyze.OverSatisfied imply T1>=Delay1

與

A<>( T1

類似地，可驗證延遲觸發(fā)時間特性“如果函數(shù)compare()在延遲時間Delay2結(jié)束后仍然等于1，則變遷analyze2到UnderSatisfied發(fā)生”。延遲觸發(fā)時間特性描述與驗證結(jié)果如圖6所示。

4.2 自適應軟件截止時間驗證

以圖5(c)為例，該截止時間特性可描述為“變遷從RemoveResource到PlanReady1的時間不能超過D”。上述性質(zhì)成立需同時滿足兩個條件：1) 若變遷從RemoveResource到PlanReady1發(fā)生，則T<=D；2) 當T>D時，變遷從RemoveResource到PlanReady1不允許發(fā)生。該截止時間用以限制函數(shù)remove()在D時間內(nèi)必須執(zhí)行完畢。上述條件可形式化描述為：

Plan.RemoveResource-->Plan.PlanReady1 imply T<=D

與

A<> T>D imply not Plan.PlanReady1

類似地，可驗證截止時間特性“變遷從AddResource到PlanReady2的時間不能超過D”，截止時間形式化描述與驗證結(jié)果如圖7所示。

圖5 自適應軟件動態(tài)過程時間特性建模模板 Fig. 5 Modeling templates of temporal properties of self-adaptive software dynamic processes

本節(jié)以3.2節(jié)建立的自適應軟件形式化模板為基礎，給出了自適應軟件延遲觸發(fā)時間和截止時間的驗證方法，具有一般應用意義。針對自適應調(diào)節(jié)時間和穩(wěn)定時間的分析將在第5章結(jié)合具體案例詳細說明。

圖6 自適應軟件延遲觸發(fā)時間形式化描述與驗證 Fig. 6 Formal description and verification of self-adaptive software delay trigger temporal properties

圖7 自適應軟件截止時間形式化描述與驗證 Fig. 7 Formal description and verification of self-adaptive software deadline temporal properties

5 案例研究

本章將以2.2節(jié)自適應場景為例，應用第3章提出的自適應軟件動態(tài)過程形式化建模模板和第4章提出的自適應性質(zhì)描述方法進行系統(tǒng)建模和性質(zhì)驗證。

5.1 艦船保障自適應信息系統(tǒng)形式化建模

圖8展示了該自適應系統(tǒng)的形式化模型，本文定義了兩個Dynamics模型分別模擬CPU利用率突然上升和突然下降的場景，自適應邏輯Monitor-Analyze-Plan-Execute和應用邏輯ServerPool構(gòu)成了自適應閉環(huán)反饋系統(tǒng)。其中Monitor定期監(jiān)控(周期為T1)服務器池ServerPool中服務器的CPU利用率(變量Utili)并將其傳給變量Data，若Data越限，將通過觸發(fā)標志flagA觸發(fā)Analyze；在Analyze中將持續(xù)監(jiān)控Delay1或Delay2時間段，若變量Data在該延遲時間段內(nèi)仍然越限，則判定系統(tǒng)為“過滿足(OverSatisfied)”或“不滿足(UnderSatisfied)”狀態(tài)，并通過flagP觸發(fā)Plan；在Plan階段根據(jù)系統(tǒng)偏離正常值的程度(以變量DUm和DUM表示)規(guī)劃自適應策略，在此定義了時間約束T4限制remove()和add()函數(shù)的執(zhí)行時間小于2個時間單位，Plan通過flagE觸發(fā)Execute；在Execute階段執(zhí)行自適應策略，類似地，定義時間約束T5限制其執(zhí)行時間，Execute通過觸發(fā)標志flagAction將自適應動作施加到ServerPool上；應用邏輯ServerPool通過增/減投運服務器的數(shù)量SerNum使CPU利用率恢復正常狀態(tài)。

5.2 艦船保障自適應信息系統(tǒng)形式化驗證

5.1節(jié)的形式化模型構(gòu)成了時間自動機網(wǎng)絡模型：TAN={Monitor,Analyze,Plan,Execute,ServerPool,Dynamics}，通過將其載入UPPAAL模擬器和驗證器可進行自動化模擬分析和形式化驗證。

1)系統(tǒng)有無死鎖。輸入命令A[ ]not deadlock檢測系統(tǒng)是否有死鎖現(xiàn)象，若存在死鎖，通過模擬器 simulator模擬自適應行為，找到發(fā)生死鎖時各自動機所處狀態(tài)，及時調(diào)整模型，其驗證結(jié)果如圖9所示。

2)自適應動作有效性。該性質(zhì)用于驗證自適應軟件的自適應動作能否得到有效執(zhí)行，在上述案例中提煉以下四條性質(zhì)進行驗證：

E<>ServerPool.removeRes

E<>Execute.exeRemoving

E<>ServerPool.addRes

E<>Execute.exeAdding

其驗證結(jié)果如圖9所示。

3)時間特性。為驗證艦船保障自適應信息系統(tǒng)的時間特性，本文將其分為延遲觸發(fā)時間、截止時間、自適應調(diào)節(jié)時間和穩(wěn)定時間等性質(zhì)進行驗證。根據(jù)第4章時間特性形式化描述模板，應用案例的延遲觸發(fā)時間和截止時間的形式化描述如表2所示，其驗證結(jié)果如圖9所示。其中，圖9(a)驗證了在應用案例CPU利用率突然上升時，自適應軟件動態(tài)過程的時間特性是否滿足；圖9(b)驗證了在應用案例CPU利用率突然下降時，自適應軟件動態(tài)過程的時間特性是否滿足。

圖8 艦船保障自適應信息系統(tǒng)形式化模型 Fig. 8 Formal model of self-adaptive ship supplying information system 表2 應用案例時間特性形式化描述 Tab. 2 Formal descriptions of temporal properties for the application example

類別應用案例時間特性提取時間特性形式化描述Analyze延遲觸發(fā)時間若CPU利用率在Delay1時間內(nèi)均高于上限值則觸發(fā)自適應行為Analyze.analyze1-->Analyze.OverSatisfiedimplyT2>=Delay1A<>(T2Analyze.UnderSatisfiedimplyT3>=Delay2A<>(T3Plan.ready1implyT4<=2A<>T4>2implynotPlan.ready1函數(shù)Add()運行時間不允許超過2個時間單位Plan.AddResource-->Plan.ready2implyT4<=2A<>T4>2implynotPlan.ready2Execute截止時間Execute執(zhí)行時間不允許超過2個時間單位Execute.wait-->Execute.endimplyT5<=2A<>T5>2implynotExecute.end系統(tǒng)反應截止時間函數(shù)removeResource()運行時間不允許超過2個時間單位ServerPool.removeRes-->ServerPool.endimplyT6<=2A<>T6>2implynotServerPool.end函數(shù)addResource()運行時間不允許超過2個時間單位ServerPool.addRes-->ServerPool.endimplyT6<=2A<>T6>2implynotServerPool.end

通過在UPPAAL中模擬仿真所建立的形式化模型，記錄了案例模型在不同自適應場景下CPU利用率Utilization隨時間t的變化過程，得到應用案例的自適應調(diào)節(jié)時間特性和自適應穩(wěn)定時間特性，如圖10所示。在CPU利用率突然下降時，系統(tǒng)通過自適應調(diào)節(jié)，經(jīng)過17個單位時間后CPU利用率恢復到上下限以內(nèi)(30%)，由于監(jiān)控的延時性，自適應過程繼續(xù)作用，系統(tǒng)經(jīng)30個單位時間恢復穩(wěn)定狀態(tài)(55%)，如圖10(a)所示。類似地，在CPU利用率突然上升時，系統(tǒng)經(jīng)過16個單位時間恢復到上下限范圍，并保持在穩(wěn)定狀態(tài)(74%)。

圖9 應用案例形式化驗證結(jié)果 Fig. 9 Formal verification results of the application example

5.3 討論

從5.2節(jié)實驗結(jié)果可以看出，本文方法除了支持系統(tǒng)死鎖和自適應動作有效性等自適應動態(tài)過程行為的分析和驗證外，還能有效支持自適應軟件時間特性的分析。在表2中描述了案例系統(tǒng)對延遲觸發(fā)時間和截止時間等特性的設計要求，并給出了相應要求的形式化描述，在圖9中通過將上述性質(zhì)載入UPPAAL可以直觀地驗證延遲觸發(fā)時間和截止時間是否得到滿足。針對自適應調(diào)節(jié)時間和自適應穩(wěn)定時間不能夠直接進行驗證，需通過分析系統(tǒng)模擬仿真軌跡(trace)建立監(jiān)控變量和時間的關(guān)系進行分析，如圖10所示，可以直觀分析CPU利用率隨時間的變化，并根據(jù)圖4中的定義確定自適應調(diào)節(jié)時間和自適應穩(wěn)定時間，判斷其是否滿足用戶需求。綜上所示，本文方法能夠直觀和有效地進行自適應軟件時間特性的分析和驗證。

圖10 應用案例的自適應調(diào)節(jié)時間和自適應穩(wěn)定時間特性 Fig. 10 Self-adaptative adjusting time property and self-adaptative steady time property of the application example

6 結(jié)語

自適應軟件的建模與驗證方法研究已成為軟件工程領域的前沿熱點研究問題。在現(xiàn)有自適應建模與驗證方法中較少考慮系統(tǒng)的時間約束，然而，在時間攸關(guān)應用領域，自適應軟件的正確運行不僅依賴于自適應邏輯的正確性，而且依賴于自適應軟件動態(tài)過程的時間特性。為此，本文定義了監(jiān)控周期以顯式刻畫監(jiān)控Monitor的時間特性；定義了延遲觸發(fā)時間，來刻畫類似“ifUtilization>MforNseconds”這種分析Analyze階段的延遲性；定義了自適應過程截止時間，用以約束Plan、Execute等的執(zhí)行時間，以降低自適應邏輯的時間開銷；定義了自適應調(diào)節(jié)時間和穩(wěn)定時間以定量評估自適應邏輯的響應速度和響應效果。此外，本文還定義了一種基于時間自動機網(wǎng)絡的自適應軟件動態(tài)過程時間特性建模模板，實現(xiàn)建模方法的復用，降低自適應軟件形式化建模難度。最后，本文將自適應軟件時間特性形式化描述為TCTL形式，并載入到時間自動機工具UPPAAL中，進行自適應軟件動態(tài)過程時間特性的形式化分析和驗證。本文以艦船保障自適應信息系統(tǒng)為例，分析和驗證了在遭受不同環(huán)境變化時系統(tǒng)的自適應行為和自適應動態(tài)過程的時間特性，從而驗證了本文方法的有效性。

本文用時間自動機模型刻畫自適應軟件的動態(tài)過程，當系統(tǒng)規(guī)模和復雜度較大時，建模難度增大，系統(tǒng)模型檢驗時會出現(xiàn)狀態(tài)空間爆炸(state-space explosion)的問題，下一步考慮將自動機模型與Event-B[18]模型相結(jié)合，構(gòu)建一種逐步精化(stepwise refinement)的自適應軟件形式化方法，降低其建模難度。

參考文獻(References)

[1] SALEHIE M, TAHVILDARI L. Self-adaptive software: landscape and research challenges [J]. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 2009, 4(2): Article No. 14.

[2] CHENG B H C, de LEMOS R, GIESE H, et al. Software engineering for self-adaptive systems: a second research roadmap [M]// Software Engineering for Self-Adaptive Systems, LNCS 5525. Berlin: Springer, 2013: 1-26.

[3] KRUPITZER C, ROTH F M, VANSYCKEL S, et al. A survey on engineering approaches for self-adaptive systems [J]. Pervasive and Mobile Computing, 2015, 17(Part B): 184-206.

[4] 楊啟亮,馬曉星,邢建春,等.軟件自適應:基于控制理論的方法[J].計算機學報,2016,39(11):2189-2215.(YANG Q L, MA X X, XING J C, et al. Software self-adaptation: control theory based approach [J]. Chinese Journal of Computers, 2016, 39(11): 2189-2215.)

[5] de la IGLESIA D G, WEYNS D. MAPE-K formal templates to rigorously design behaviors for self-adaptive systems [J]. ACM Transactions on Autonomous & Adaptive Systems, 2015, 10(3): Article No. 15.

[6] VOGEL T, GIESE H. Model-driven engineering of self-adaptive software with EUREMA [J]. ACM Transactions on Autonomous & Adaptive Systems , 2014, 8(4): Article No. 18.

[7] 韓德帥,楊啟亮,邢建春.一種軟件自適應UML建模及其形式化驗證方法[J].軟件學報,2015,26(4):730-746.(HAN D S, YANG Q L, XING J C. UML-based modeling and formal verification for software self-adaptation [J]. Journal of Software, 2015, 26(4): 730-746.)

[8] HAN D, YANG Q, XING J, et al. FAME: a UML-based framework for modeling fuzzy self-adaptive software [J]. Information & Software Technology, 2016, 76: 118-134.

[9] MURCH R. Autonomic Computing [M]. [S.l.]: IBM Press, 2004: 535-539.

[10] RAMIREZ A J, CHENG B H C. Design patterns for developing dynamically adaptive systems [C]// SEAMS ’10: Proceedings of the 2010 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems. New York: ACM, 2010: 49-58.

[11] BARTELS B, KLEINE M. A CSP-based framework for the specification, verification, and implementation of adaptive systems [C]// SEAMS ’11: Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-Managing Systems. New York: ACM, 2011: 158-167.

[12] CALINESCU R, GHEZZI C, KWIATKOWSKA M, et al. Self-adaptive software needs quantitative verification at runtime [J]. Communications of the ACM, 2012, 55(9): 69-77.

[13] DING Z, ZHOU Y, ZHOU M. Modeling self-adaptive software systems with learning Petri nets [J]. IEEE Transactions on Systems, Man, and Cybernetics Systems, 2016, 46(4): 483-498.

[14] WEYNS D, IFTIKHAR M U, de la IGLESIA D G, et al. A survey of formal methods in self-adaptive systems [C]// C3S2E ’12: Proceedings of the 5th International C*Conference on Computer Science and Software Engineering. New York: ACM, 2012: 67-79.

[15] CAMILLI M, GARGANTINI A, SCANDURRA P. Specifying and verifying real-time self-adaptive systems [C]// ISSRE 2015: Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering. Piscataway, NJ: IEEE, 2015: 303-313.

[16] HACHICHA M, HALIMA R B, KACEM A H. Modeling and verifying self-adaptive systems: a refinement approach [C]// SMC 2016: Proceedings of the 2016 IEEE International Conference on Systems, Man, and Cybernetics. Piscataway, NJ: IEEE, 2016: 3967-3972.

[17] ABRIAL J R. Modeling in Event-B: System and Software Engineering [M]. Cambridge, UK: Cambridge University Press, 2010: 176.

[18] FILIERI A, GHEZZI C, TAMBURRELLI G. A formal approach to adaptive software: continuous assurance of non-functional requirements [J]. Formal Aspects of Computing, 2012, 24(2): 163-186.

[19] GHEZZI C, PINTO L S, SPOLETINI P, et al. Managing non-functional uncertainty via model-driven adaptivity [C]// ICSE ’13: Proceedings of the 2013 International Conference on Software Engineering. Piscataway, NJ: IEEE, 2013: 33-42.

[20] KEPHART J O, CHESS D M. The vision of autonomic computing [J]. IEEE Computer, 2003, 36(1): 41-50.

[21] HAN D, XING J, YANG Q, et al. Handling uncertainty in self-adaptive software using self-learning fuzzy neural network [C]// COMPSAC 2016: Proceedings of the 40th IEEE Annual Computer Software and Applications Conference. Washington, DC: IEEE Computer Society, 2016: 540-545.

[22] ALUR R, DILL D L. A theory of timed automata [J]. Theoretical Computer Science, 1994, 126(2): 183-235.

[23] LARSEN K G, PETTERSSON P, YI W. UPPAAL in a Nutshell [J]. International Journal on Software Tools for Technology Transfer, 1997, 1(1/2): 134-152.

This work is supported by the Natural Science Foundation of Jiangsu Province (BK20151451).

HANDeshuai, born in 1990, Ph. D. candidate. His research interests include software self-adaptation, Cyber-Physical System (CPS).

XINGJianchun, born in 1964, Ph. D., professor. His research interests include Cyber-Physical System (CPS), Building Information Model (BIM).

YANGQiliang, born in 1975, Ph. D., associate professor. His research interests include software self-adaptation, Building Information Model (BIM).

LIJuelong, born in 1959, M. S., professor. His research interests include building environment and equipment engineering.