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

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

0 引言

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

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

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

1 相關(guān)工作

軟件自適應(yīng)已成為軟件工程領(lǐng)域所關(guān)注的一個焦點(diǎ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)研討會、《軟件學(xué)報》自適應(yīng)軟件?？戎卸伎煽闯鲕浖赃m應(yīng)問題研究的重要性，其中針對自適應(yīng)軟件的形式化建模方法的研究也吸引了眾多研究學(xué)者。

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

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

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

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

2 自適應(yīng)軟件時間特性定義

2.1 自適應(yīng)軟件MAPE-K模型

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

圖1 MAPE-K自適應(yīng)軟件模型 Fig. 1 MAPE-K self-adaptive software model

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

2.2 典型自適應(yīng)場景

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

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

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

2.3 自適應(yīng)軟件時間特性分析與定義

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

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

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

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

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

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

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

3.1 時間自動機(jī)模型

時間自動機(jī)模型(timed automata)[22]對傳統(tǒng)有限自動機(jī)模型進(jìn)行了擴(kuò)展，加入了時間約束，以支持對系統(tǒng)實(shí)時特性的描述和形式化分析，其可定義為一個六元組：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ā)時間自動機(jī)模型可組成一個時間自動機(jī)網(wǎng)絡(luò)模型(Timed Automata Network, TAN)，記為：TAN≡TA1‖TA2‖…‖TAn。

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

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

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

具體而言，監(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ù)和設(shè)定的上下限比較，確定監(jiān)控數(shù)據(jù)低于下限狀態(tài)“l(fā)ow”或高于上限狀態(tài)“high”或處于上下限之間“NoChange”，并根據(jù)不同狀態(tài)觸發(fā)不同分析標(biāo)志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ā)相應(yīng)的規(guī)劃標(biāo)志flagP。

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

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

4 自適應(yīng)軟件時間特性分析與驗(yàn)證

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

4.1 自適應(yīng)軟件延遲觸發(fā)時間驗(yàn)證

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

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

與

A<>( T1

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

4.2 自適應(yīng)軟件截止時間驗(yàn)證

以圖5(c)為例，該截止時間特性可描述為“變遷從RemoveResource到PlanReady1的時間不能超過D”。上述性質(zhì)成立需同時滿足兩個條件：1) 若變遷從RemoveResource到PlanReady1發(fā)生，則T<=D；2) 當(dāng)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

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

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

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

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

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

5 案例研究

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

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

圖8展示了該自適應(yīng)系統(tǒng)的形式化模型，本文定義了兩個Dynamics模型分別模擬CPU利用率突然上升和突然下降的場景，自適應(yīng)邏輯Monitor-Analyze-Plan-Execute和應(yīng)用邏輯ServerPool構(gòu)成了自適應(yīng)閉環(huán)反饋系統(tǒng)。其中Monitor定期監(jiān)控(周期為T1)服務(wù)器池ServerPool中服務(wù)器的CPU利用率(變量Utili)并將其傳給變量Data，若Data越限，將通過觸發(fā)標(biāo)志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ī)劃自適應(yīng)策略，在此定義了時間約束T4限制remove()和add()函數(shù)的執(zhí)行時間小于2個時間單位，Plan通過flagE觸發(fā)Execute；在Execute階段執(zhí)行自適應(yīng)策略，類似地，定義時間約束T5限制其執(zhí)行時間，Execute通過觸發(fā)標(biāo)志flagAction將自適應(yīng)動作施加到ServerPool上；應(yīng)用邏輯ServerPool通過增/減投運(yùn)服務(wù)器的數(shù)量SerNum使CPU利用率恢復(fù)正常狀態(tài)。

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

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

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

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

E<>ServerPool.removeRes

E<>Execute.exeRemoving

E<>ServerPool.addRes

E<>Execute.exeAdding

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

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

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

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

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

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

5.3 討論

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

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

6 結(jié)語

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

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

參考文獻(xiàn)(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] 楊啟亮,馬曉星,邢建春,等.軟件自適應(yīng):基于控制理論的方法[J].計算機(jī)學(xué)報,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] 韓德帥,楊啟亮,邢建春.一種軟件自適應(yīng)UML建模及其形式化驗(yàn)證方法[J].軟件學(xué)報,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.