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

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

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

0 引言

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

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

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

1 相關工作

軟件自適應已成為軟件工程領域所關注的一個焦點問題，從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)研討會、《軟件學報》自適應軟件專刊等中都可看出軟件自適應問題研究的重要性，其中針對自適應軟件的形式化建模方法的研究也吸引了眾多研究學者。

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

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

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

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

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

2.1 自適應軟件MAPE-K模型

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

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

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

2.2 典型自適應場景

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

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

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

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

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

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

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

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

圖4 自適應調節時間和穩定時間示意 Fig. 4 Self-adaptive adjusting time and steady time

3 自適應軟件動態過程時間特性建模

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

3.1 時間自動機模型

時間自動機模型(timed automata)[22]對傳統有限自動機模型進行了擴展，加入了時間約束，以支持對系統實時特性的描述和形式化分析，其可定義為一個六元組：TA〈L,l0,S,A,E,I〉。其中：L是有限位置的集合，L?Location；l0∈L表示初始位置initiallocation；S是邊E上約束的集合，S?Guard；A是所有動作的集合，包括輸入、輸出和內部三類動作，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′ 的遷移，遷移過程伴有衛式約束g、賦值操作u和動作a；I是不變式invariant的集合；I?Guard用以約束位置的狀態。

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

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

3.2 自適應軟件動態過程時間特性建模模板

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

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

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

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

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

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

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

4.1 自適應軟件延遲觸發時間驗證

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

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

與

A<>( T1

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

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

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

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

與

A<> T>D imply not Plan.PlanReady1

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

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

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

圖6 自適應軟件延遲觸發時間形式化描述與驗證 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節自適應場景為例，應用第3章提出的自適應軟件動態過程形式化建模模板和第4章提出的自適應性質描述方法進行系統建模和性質驗證。

5.1 艦船保障自適應信息系統形式化建模

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

5.2 艦船保障自適應信息系統形式化驗證

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

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

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

E<>ServerPool.removeRes

E<>Execute.exeRemoving

E<>ServerPool.addRes

E<>Execute.exeAdding

其驗證結果如圖9所示。

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

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

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

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

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

5.3 討論

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

圖10 應用案例的自適應調節時間和自適應穩定時間特性 Fig. 10 Self-adaptative adjusting time property and self-adaptative steady time property of the application example

6 結語

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

本文用時間自動機模型刻畫自適應軟件的動態過程，當系統規模和復雜度較大時，建模難度增大，系統模型檢驗時會出現狀態空間爆炸(state-space explosion)的問題，下一步考慮將自動機模型與Event-B[18]模型相結合，構建一種逐步精化(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.