摘 要：基于自適應(yīng)UMI軟件開發(fā)效率提升的要求以及自適應(yīng)軟件可靠性的保障要求，此次研究提出了MV4SAS方法，其促進(jìn)了可視化UML與嚴(yán)格化時(shí)間自動機(jī)的有機(jī)結(jié)合，能夠?qū)崿F(xiàn)軟件自適應(yīng)建模與形式化驗(yàn)證，首先在UML擴(kuò)展機(jī)制作用下引入新的構(gòu)造型、標(biāo)記值以及約束條件等，在軟件自適應(yīng)建模設(shè)施基礎(chǔ)上構(gòu)造相應(yīng)的軟件自適應(yīng)結(jié)構(gòu)模型與行為模型，并通過轉(zhuǎn)換算法實(shí)現(xiàn)軟件自適應(yīng)行為模型向時(shí)間自動機(jī)網(wǎng)絡(luò)的轉(zhuǎn)換，構(gòu)建軟件自適應(yīng)形式化模型，對軟件自適應(yīng)形式化驗(yàn)證的性質(zhì)進(jìn)行定義，利用模型檢測工具UPPAAL對軟件自適應(yīng)模型的可靠性進(jìn)行驗(yàn)證，結(jié)果顯示該方法能夠在一定程度上降低軟件自適應(yīng)建模與驗(yàn)證的復(fù)雜性，提升建模效率，可靠性高，值得參考借鑒。

關(guān)鍵詞：MV4SAS；軟件自適應(yīng)；UML建模；形式化驗(yàn)證

中圖分類號：TP311.11 文獻(xiàn)標(biāo)識碼：A

1 引言（Introduction）

隨著現(xiàn)代科學(xué)技術(shù)的不斷發(fā)展，我國的軟件規(guī)模復(fù)雜程度及用戶的需求不斷加大，這也在一定程度上對軟件運(yùn)行、維護(hù)提出了更大的挑戰(zhàn)[1]，在這樣的發(fā)展環(huán)境下，軟件自適應(yīng)技術(shù)應(yīng)運(yùn)而生，其能夠增強(qiáng)軟件的環(huán)境適應(yīng)能力，滿足用戶多變的需求，在運(yùn)行過程中根據(jù)軟件信息對相關(guān)參數(shù)、結(jié)構(gòu)等進(jìn)行調(diào)整，消除軟件運(yùn)行變化帶來的消極影響，確保軟件服務(wù)能力的提升，因此，對軟件自適應(yīng)UML建模及其形式化驗(yàn)證方法的研究有著重要的實(shí)踐意義與應(yīng)用價(jià)值。

2 預(yù)備知識概述（Summary of preliminary

knowledge）

2.1 軟件自適應(yīng)概念模型

作為軟件自適應(yīng)研究的前提與基礎(chǔ)，概念模型受到了國內(nèi)外學(xué)者的廣泛關(guān)注，國外學(xué)者提出的軟件自適應(yīng)概念模型主要包括MAPE-K自治計(jì)算模型、監(jiān)視—探測—決策—行動軟件自適應(yīng)模型等[2，3]，我國學(xué)者針對群體自適應(yīng)提出了Auxo模型，面向復(fù)雜信息系統(tǒng)提出了軟件模糊自適應(yīng)SFSA模型，其適應(yīng)的領(lǐng)域不同，然而都體現(xiàn)了感知—決策—執(zhí)行自適應(yīng)環(huán)的內(nèi)涵與價(jià)值[4]。在自適應(yīng)目標(biāo)驅(qū)動下，軟件能夠根據(jù)運(yùn)行環(huán)境及自身狀態(tài)的變化對行為做出適當(dāng)?shù)恼{(diào)整，完成自適應(yīng)環(huán)與運(yùn)行環(huán)境、用戶等之間的交互。此次研究對原有的MAPE-K模型進(jìn)行了相應(yīng)的改進(jìn)，具體見圖1，該自適應(yīng)軟件系統(tǒng)主要包括自適應(yīng)邏輯單元與應(yīng)用邏輯單元，自適應(yīng)邏輯單元中的各個(gè)模塊共享一個(gè)知識庫構(gòu)建，此次研究將以該框架為原型構(gòu)建軟件自適應(yīng)結(jié)構(gòu)模型。

2.2 UML及其擴(kuò)展機(jī)制概述

作為一種面向?qū)ο蟮目梢暬ＵZ言，統(tǒng)一建模語言（UML）能夠提供多種圖元，從多個(gè)視角與層次對復(fù)雜軟件的結(jié)構(gòu)、特性進(jìn)行描述，在各個(gè)領(lǐng)域中均有著廣泛地應(yīng)用。UML模型主要包括結(jié)構(gòu)模型與行為模型兩種，常見的典型結(jié)構(gòu)視圖有構(gòu)件圖、類圖等，行為視圖有狀態(tài)圖、序列圖等[5]。以類圖為例，其是軟件結(jié)構(gòu)模型可視化、文檔化的重要條件，盡管其在運(yùn)行過程中包含部分具體化行為元素，然而其主要根據(jù)其他視圖刻畫動態(tài)特征。從當(dāng)前UML的建模設(shè)施現(xiàn)狀看，其能夠滿足大多數(shù)領(lǐng)域需求，然而對于部分特定領(lǐng)域還缺乏一定的建模能力，必須對其進(jìn)行適當(dāng)?shù)臄U(kuò)展，要求在原模型的基礎(chǔ)上作出通用的擴(kuò)展，常見的有增加新屬性、添加建模設(shè)施、增加語義描述等。

2.3 時(shí)間自動機(jī)理論與形式化驗(yàn)證工具

為了有效解決實(shí)時(shí)系統(tǒng)建模及驗(yàn)證問題，可以對自動機(jī)理論作出新的擴(kuò)展，即時(shí)間自動機(jī)，其能夠通過簡單的方法對包含時(shí)間因素的系統(tǒng)進(jìn)行描述，進(jìn)而為實(shí)時(shí)系統(tǒng)行為建模及性能分析提供形式化模型。國外學(xué)者根據(jù)時(shí)間自動機(jī)理論提出了UPPAAL、SPIN模型檢測工具[3，4]。以UPPAAL模型檢測工具為例，其主要采用了整型變量時(shí)間自動機(jī)網(wǎng)絡(luò)模擬實(shí)時(shí)系統(tǒng)及時(shí)序邏輯TCTL刻畫系統(tǒng)性質(zhì)，在有限狀態(tài)搜集驗(yàn)證系統(tǒng)的作用下，判斷系統(tǒng)能夠達(dá)到期望性質(zhì)[6]。其性質(zhì)驗(yàn)證規(guī)范語言的語法為。

3 基于MV4SAS軟件自適應(yīng)UML建模及其形式

化驗(yàn)證方法（Adaptive UML modeling based

on MV4SAS software and its formal verification

method）

盡管UML建模語言具有可視化特征，便于理解、交流能夠達(dá)到國際工業(yè)標(biāo)準(zhǔn)，然而由于模型檢測形式化語義的缺乏，其對軟件模型的描述很大程度上是半形式化。基于自動機(jī)嚴(yán)格語法、語義的特點(diǎn)，其能夠?qū)崿F(xiàn)軟件行為分析、求精與驗(yàn)證，然而，缺乏直觀性，為軟件開發(fā)人員的理解帶來了一定的難度。UML與自動機(jī)在模型驗(yàn)證及軟件建模等方面有著較高的互補(bǔ)性[7]，因此，可以采用UML可視化建模方法與時(shí)間自動機(jī)進(jìn)行形式化建模相結(jié)合的方式，通過融合擴(kuò)展對UML及自動機(jī)軟件自適應(yīng)建模進(jìn)行形式化驗(yàn)證，其具體過程如圖2所示。首先，要構(gòu)建軟件自適應(yīng)可視化模型，在MAPE-K改進(jìn)模型擴(kuò)展及UML模型裁剪的基礎(chǔ)上，構(gòu)建自適應(yīng)類圖，對自適應(yīng)軟件的結(jié)構(gòu)特征進(jìn)行描述，然后經(jīng)過轉(zhuǎn)換作用，使軟件自適應(yīng)可視化模型轉(zhuǎn)變?yōu)樾问交Ｐ?，并通過定義模型轉(zhuǎn)換算法，實(shí)現(xiàn)可視化自適應(yīng)序列圖向形式化時(shí)間自動機(jī)網(wǎng)絡(luò)的轉(zhuǎn)換，構(gòu)建軟件自適應(yīng)形式化模型，最后對上述模型的可靠性進(jìn)行驗(yàn)證。

4 UML擴(kuò)展的軟件自適應(yīng)建模（UML extended

software adaptive modeling）

4.1 自適應(yīng)類圖

類圖主要指的是對軟件結(jié)構(gòu)的可視化描述，此次研究對UML類圖進(jìn)行了擴(kuò)展，添加了部分軟件自適應(yīng)建模設(shè)施，構(gòu)建了面向軟件的自適應(yīng)結(jié)構(gòu)模型，該自適應(yīng)類圖模型包含一個(gè)四元組ACD：=（CA，RA，AA，SA），其中CA表示的是自適應(yīng)類有限集合，CA={監(jiān)視，分析，計(jì)劃，執(zhí)行，知識庫，用戶，環(huán)境}。RA表示的是自適應(yīng)關(guān)系有限集合，，RA表示的是基于UML的關(guān)系構(gòu)造，其能夠體現(xiàn)出自適應(yīng)軟件各功能單元之間的連接關(guān)系。AA表示的是自適應(yīng)屬性集合，其中部分屬性采用標(biāo)記值的方式附加在CA構(gòu)造型中，，其中A表示的是Class屬性Attribute的集合，Tag表示的是添加標(biāo)記值的集合，能夠應(yīng)用于刻畫顯示性功能單元的類型與屬性[8]。約束條件集合則采用SA表示，，分別表示時(shí)間約束與事件約束，此次研究在描述定義約束條件時(shí)采用的是對象約束語言O(shè)CL。此次研究要求在MAPE-K環(huán)的每個(gè)單元都能夠上升一階要素實(shí)施描述、刻畫，與此同時(shí)，受軟件自適應(yīng)環(huán)與用戶、軟件運(yùn)行環(huán)境以及動態(tài)交互等過程的影響，可以對用戶、環(huán)境及軟件等進(jìn)行獨(dú)立實(shí)體描述，另外可以將復(fù)合結(jié)構(gòu)的類如CA元素泛化成為具體的類。在擴(kuò)展UML的作用下，自適應(yīng)類圖能夠構(gòu)建自適應(yīng)關(guān)系，并通過軟件對自適應(yīng)類交互關(guān)系進(jìn)行刻畫，其語義描述如表1所示。

4.2 自適應(yīng)序列圖

UML序列圖主要是對對象之間動態(tài)交互關(guān)系的描述，其能夠?qū)坍媽ο笙鬟f時(shí)間順序，以及系統(tǒng)預(yù)期功能等做出準(zhǔn)確的反應(yīng)，然而UML序列圖也具有自身的缺陷性，其不能夠?qū)蝹€(gè)對象某一時(shí)間段內(nèi)的活躍狀態(tài)進(jìn)行反映，加大了形式化驗(yàn)證的難度，此次研究通過橫向與縱向兩個(gè)維度對UML序列圖進(jìn)行擴(kuò)展，并對軟件自適應(yīng)行為模型做出了定義。自適應(yīng)序列圖為一個(gè)五元組，具體表示為，其中軟件自適應(yīng)過程對象有限集合采用OA表示，OA={監(jiān)視，分析，規(guī)劃，執(zhí)行，知識庫，用戶，環(huán)境}。對象生命線上狀態(tài)有限集合采用STA表示，ST*A表示的是除去空事件的所有不重復(fù)狀態(tài)集合，即。MA表示的是有窮消息集合，與此同時(shí)自適應(yīng)序列圖還在UML序列圖基礎(chǔ)上對sim、alt和loop三個(gè)片段進(jìn)行了定義，可以表示為FG=，每一個(gè)片段都有片段名與執(zhí)行條件構(gòu)成，其中sim表示的是簡單片段，執(zhí)行條件為空，alt則為分支選擇片段，其下一狀態(tài)流向往往由執(zhí)行條件決定。而loop則為循環(huán)片段，當(dāng)條件為真，那么其包含的對象能夠轉(zhuǎn)化成為激活狀態(tài)。約束有限集合采用SA表示，具體表示為，分別代表的是狀態(tài)內(nèi)部與狀態(tài)之間的約束集合狀態(tài)。自適應(yīng)序列圖也可以采用二維表表示，用橫向表示空間軸，代表參與自適應(yīng)協(xié)作的對象集合；縱向則表示時(shí)間軸，代表對象生命線，其能夠反映出單個(gè)對象對一定時(shí)間內(nèi)的活躍情況。另外，自適應(yīng)序列圖還對組合片段與約束的概念進(jìn)行了強(qiáng)化，體現(xiàn)了軟件自適應(yīng)實(shí)時(shí)性的特征。此次研究的自適應(yīng)序列激昂UML序列圖與狀態(tài)圖進(jìn)行了無縫銜接，不僅能夠?qū)ψ赃m應(yīng)環(huán)中的各個(gè)軟件實(shí)體交互關(guān)系進(jìn)行刻畫，而且能夠?qū)μ囟ㄖ芷趦?nèi)單個(gè)軟件實(shí)體的活躍狀態(tài)進(jìn)行準(zhǔn)確描述，與此同時(shí)在形式化定義作用下，其能夠?qū)崿F(xiàn)向時(shí)間自動機(jī)模型的有效轉(zhuǎn)化，進(jìn)而為軟件自適應(yīng)形式化驗(yàn)證奠定堅(jiān)實(shí)的基礎(chǔ)。

4.3 基于UML擴(kuò)展的軟件自適應(yīng)建模原則

此次研究軟件自適應(yīng)建立的本質(zhì)為自適應(yīng)環(huán)（監(jiān)視、分析、規(guī)劃、執(zhí)行）與不斷變化軟件的交互，因此必須將參與自適應(yīng)過程的軟件實(shí)體及自適應(yīng)環(huán)作為一階要素給予顯示化建模與刻畫。其次，要遵循自適應(yīng)邏輯外置分離原則，一般可采用外置式方式，從目標(biāo)軟件系統(tǒng)中對自適應(yīng)邏輯進(jìn)行分離，這能夠在一定程度上避免應(yīng)用邏輯與自適應(yīng)邏輯之間的交織。除此之外，還必須遵循約束條件規(guī)范描述原則，對時(shí)間約束與事件約束進(jìn)行相應(yīng)的規(guī)范，其能夠?yàn)檐浖赃m應(yīng)UML模型轉(zhuǎn)換奠定基礎(chǔ)。

5 軟件自適應(yīng)模型轉(zhuǎn)換與形式化驗(yàn)證（Software

adaptive model transformation and formal

verification）

5.1 軟件自適應(yīng)UMI模型向時(shí)間自動機(jī)模型的轉(zhuǎn)換

通常，自適應(yīng)序列圖ASD能夠?qū)r(shí)間自動機(jī)網(wǎng)絡(luò)，以及生命周期狀態(tài)變化情況進(jìn)行映射與刻畫；自適應(yīng)序列圖的狀態(tài)即State則能夠有效映射時(shí)間自動機(jī)位置，每個(gè)自動機(jī)TA的位置集合均有相應(yīng)的對象縱軸狀態(tài)集合表示，且ASD縱軸初始狀態(tài)一般對應(yīng)的是時(shí)間自動機(jī)的初始位置。自適應(yīng)序列圖消息message則被映射成為時(shí)間自動機(jī)通道，且每個(gè)消息都恰好與時(shí)間自動機(jī)的發(fā)送事件、接收事件一一對應(yīng)。另外時(shí)間自動機(jī)的約束S與自適應(yīng)序列圖約束SA相對應(yīng)，狀態(tài)間約束Sinter及分段約束FG則分別對應(yīng)時(shí)間自動機(jī)邊E的約束S，時(shí)間自動機(jī)位置不變式Invariant則對應(yīng)狀態(tài)內(nèi)部約束Sintra。為了確保自動機(jī)模型的有效運(yùn)行，在建模過程中，建模工作人員需要結(jié)合實(shí)際情況對自動機(jī)模型進(jìn)行優(yōu)化處理，積極處理應(yīng)用邏輯參數(shù)的動態(tài)變化，對時(shí)間自動機(jī)模型進(jìn)行進(jìn)一步完善。

5.2 軟件自適應(yīng)形式化驗(yàn)證

軟件自適應(yīng)形式化驗(yàn)證主要是對軟件可靠性、自身適應(yīng)能力及影響因素等的檢測，主要檢測的能力包括系統(tǒng)有無死鎖、自適應(yīng)規(guī)則是否正確、自適應(yīng)相應(yīng)能力是否滿足需求等[9]。（1）系統(tǒng)是否有死鎖。與傳統(tǒng)的軟件有所不同，自適應(yīng)軟件對系統(tǒng)持續(xù)運(yùn)行能力有著較高的要求，一般需要嚴(yán)密觀察自適應(yīng)軟件系統(tǒng)是否進(jìn)入死鎖狀態(tài)，避免軟件運(yùn)行中進(jìn)入到錯誤狀態(tài)。（2）自適應(yīng)動作是否有效[1]。該檢測主要針對的是自適應(yīng)動作的執(zhí)行情況，一般情況下，建模人員會事先構(gòu)建自適應(yīng)動作以便隨時(shí)應(yīng)對軟件運(yùn)行中的內(nèi)部狀態(tài)、環(huán)境及用戶需求變化，與此同時(shí)還需檢查其是否存在重復(fù)、冗余等。（3）自適應(yīng)規(guī)則正確性。該檢測針對的是系統(tǒng)應(yīng)對某種

特殊變化時(shí)的應(yīng)對情況。（4）自適應(yīng)快速反應(yīng)能力。其主要指的是觸發(fā)自適應(yīng)行為后，自適應(yīng)邏輯單元在一定時(shí)間內(nèi)的響應(yīng)速度與響應(yīng)能力，其需要確保自適應(yīng)策略的正確性與有效性。除此之外，還需要對軟件自適應(yīng)行為進(jìn)行模擬與形式化驗(yàn)證。UPPAAL所提供的simulator模擬器能夠?qū)浖赃m應(yīng)交互過程進(jìn)行模擬，并形成一個(gè)完整的運(yùn)行軌跡，若運(yùn)行出現(xiàn)錯誤，系統(tǒng)將會立即做出反饋，便于建模人員及時(shí)做出相關(guān)調(diào)整。在UPPAAL驗(yàn)證器verifier中輸入TCTL可靠性規(guī)約，系統(tǒng)能夠?qū)浖赃m應(yīng)性質(zhì)進(jìn)行自動檢測，最終得到完善的軟件自適應(yīng)模型。

6 結(jié)論（Conclusion）

傳統(tǒng)的UML具備形象、直觀等特點(diǎn)，然而缺乏科學(xué)的分析與驗(yàn)證機(jī)制，其形式化方法定義相對嚴(yán)格，不利于軟件工程師理解，基于上述因素，此次研究提出了UML擴(kuò)展與時(shí)間自動機(jī)有機(jī)融合的自適應(yīng)建模及形式化驗(yàn)證方法，其不僅降低了設(shè)計(jì)難度，而且在一定程度上提升了軟件建模的可靠性，值得廣泛推廣、應(yīng)用。

參考文獻(xiàn)（References）

[1] 趙曉宇，等.基于HUML的列控系統(tǒng)形式化建模與參數(shù)分析方法[J].鐵道學(xué)報(bào)，2016，38（11）：80-87.

[2] Thomas Vogel，Holger Giese.Model-Driven Engineering of Self-Adaptive Software with EUREMA[J].ACM Transactions on Autonomous and Adaptive Systems（TAAS），2014，8（4）：1-33.

[3] Yang ZQ，et al.A Systematic Literature Review of Requirements Modeling and Analysis for Self-Adaptive Systems.Requirements Engineering：Foundation for Software Quality，2014.

[4] 郭雨婷，潘文林，江濤.基于common logic的UML類圖形式化及驗(yàn)證[J].云南民族大學(xué)學(xué)報(bào)自然科學(xué)版，2015，22（6）：506-509.

[5] 安越，李國寧.基于Timed-UML順序圖的RBC交接形式化建模與分析[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2016，60（6）：132-138.

[6] Ding Z，Zhou Y，Zhou MC.Modeling Self-Adaptive Software Systems with Learning Petrinets.Companion Proc.of the 36th Int Conf.on Software Engineering，2014.

[7] 劉懷玉，陽西述，何昭青.算術(shù)四則運(yùn)算智能測試教學(xué)軟件的設(shè)計(jì)[J].軟件工程師，2014，13（6）：42-43.

[8] 王泊涵.一種基于UML的軟件生產(chǎn)線可變性建模與仿真驗(yàn)證方法的研究與實(shí)現(xiàn)[D].中國航天第二研究院，航天科工集團(tuán)第二研究院，2015.

[9] 雷義偉，賁可榮，何智勇.自適應(yīng)軟件需求的形式化建模與驗(yàn)證[J].海軍工程大學(xué)學(xué)報(bào)，2015，27（6）：73-78.

作者簡介：

施柏銓（1981-），男，本科，講師.研究領(lǐng)域：計(jì)算機(jī)科學(xué)與技

術(shù)學(xué)，計(jì)算機(jī)網(wǎng)絡(luò).