基于MV4SAS研究軟件自適應UML建模及其形式化驗證方法研究

摘 要：基于自適應UMI軟件開發效率提升的要求以及自適應軟件可靠性的保障要求，此次研究提出了MV4SAS方法，其促進了可視化UML與嚴格化時間自動機的有機結合，能夠實現軟件自適應建模與形式化驗證，首先在UML擴展機制作用下引入新的構造型、標記值以及約束條件等，在軟件自適應建模設施基礎上構造相應的軟件自適應結構模型與行為模型，并通過轉換算法實現軟件自適應行為模型向時間自動機網絡的轉換，構建軟件自適應形式化模型，對軟件自適應形式化驗證的性質進行定義，利用模型檢測工具UPPAAL對軟件自適應模型的可靠性進行驗證，結果顯示該方法能夠在一定程度上降低軟件自適應建模與驗證的復雜性，提升建模效率，可靠性高，值得參考借鑒。

關鍵詞：MV4SAS；軟件自適應；UML建模；形式化驗證

中圖分類號：TP311.11 文獻標識碼：A

1 引言（Introduction）

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

2 預備知識概述（Summary of preliminary

knowledge）

2.1 軟件自適應概念模型

作為軟件自適應研究的前提與基礎，概念模型受到了國內外學者的廣泛關注，國外學者提出的軟件自適應概念模型主要包括MAPE-K自治計算模型、監視—探測—決策—行動軟件自適應模型等[2，3]，我國學者針對群體自適應提出了Auxo模型，面向復雜信息系統提出了軟件模糊自適應SFSA模型，其適應的領域不同，然而都體現了感知—決策—執行自適應環的內涵與價值[4]。在自適應目標驅動下，軟件能夠根據運行環境及自身狀態的變化對行為做出適當的調整，完成自適應環與運行環境、用戶等之間的交互。此次研究對原有的MAPE-K模型進行了相應的改進，具體見圖1，該自適應軟件系統主要包括自適應邏輯單元與應用邏輯單元，自適應邏輯單元中的各個模塊共享一個知識庫構建，此次研究將以該框架為原型構建軟件自適應結構模型。

2.2 UML及其擴展機制概述

作為一種面向對象的可視化建模語言，統一建模語言（UML）能夠提供多種圖元，從多個視角與層次對復雜軟件的結構、特性進行描述，在各個領域中均有著廣泛地應用。UML模型主要包括結構模型與行為模型兩種，常見的典型結構視圖有構件圖、類圖等，行為視圖有狀態圖、序列圖等[5]。以類圖為例，其是軟件結構模型可視化、文檔化的重要條件，盡管其在運行過程中包含部分具體化行為元素，然而其主要根據其他視圖刻畫動態特征。從當前UML的建模設施現狀看，其能夠滿足大多數領域需求，然而對于部分特定領域還缺乏一定的建模能力，必須對其進行適當的擴展，要求在原模型的基礎上作出通用的擴展，常見的有增加新屬性、添加建模設施、增加語義描述等。

2.3 時間自動機理論與形式化驗證工具

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

3 基于MV4SAS軟件自適應UML建模及其形式

化驗證方法（Adaptive UML modeling based

on MV4SAS software and its formal verification

method）

盡管UML建模語言具有可視化特征，便于理解、交流能夠達到國際工業標準，然而由于模型檢測形式化語義的缺乏，其對軟件模型的描述很大程度上是半形式化。基于自動機嚴格語法、語義的特點，其能夠實現軟件行為分析、求精與驗證，然而，缺乏直觀性，為軟件開發人員的理解帶來了一定的難度。UML與自動機在模型驗證及軟件建模等方面有著較高的互補性[7]，因此，可以采用UML可視化建模方法與時間自動機進行形式化建模相結合的方式，通過融合擴展對UML及自動機軟件自適應建模進行形式化驗證，其具體過程如圖2所示。首先，要構建軟件自適應可視化模型，在MAPE-K改進模型擴展及UML模型裁剪的基礎上，構建自適應類圖，對自適應軟件的結構特征進行描述，然后經過轉換作用，使軟件自適應可視化模型轉變為形式化模型，并通過定義模型轉換算法，實現可視化自適應序列圖向形式化時間自動機網絡的轉換，構建軟件自適應形式化模型，最后對上述模型的可靠性進行驗證。

4 UML擴展的軟件自適應建模（UML extended

software adaptive modeling）

4.1 自適應類圖

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

4.2 自適應序列圖

UML序列圖主要是對對象之間動態交互關系的描述，其能夠對刻畫對象消息傳遞時間順序，以及系統預期功能等做出準確的反應，然而UML序列圖也具有自身的缺陷性，其不能夠對單個對象某一時間段內的活躍狀態進行反映，加大了形式化驗證的難度，此次研究通過橫向與縱向兩個維度對UML序列圖進行擴展，并對軟件自適應行為模型做出了定義。自適應序列圖為一個五元組，具體表示為，其中軟件自適應過程對象有限集合采用OA表示，OA={監視，分析，規劃，執行，知識庫，用戶，環境}。對象生命線上狀態有限集合采用STA表示，ST*A表示的是除去空事件的所有不重復狀態集合，即。MA表示的是有窮消息集合，與此同時自適應序列圖還在UML序列圖基礎上對sim、alt和loop三個片段進行了定義，可以表示為FG=，每一個片段都有片段名與執行條件構成，其中sim表示的是簡單片段，執行條件為空，alt則為分支選擇片段，其下一狀態流向往往由執行條件決定。而loop則為循環片段，當條件為真，那么其包含的對象能夠轉化成為激活狀態。約束有限集合采用SA表示，具體表示為，分別代表的是狀態內部與狀態之間的約束集合狀態。自適應序列圖也可以采用二維表表示，用橫向表示空間軸，代表參與自適應協作的對象集合；縱向則表示時間軸，代表對象生命線，其能夠反映出單個對象對一定時間內的活躍情況。另外，自適應序列圖還對組合片段與約束的概念進行了強化，體現了軟件自適應實時性的特征。此次研究的自適應序列激昂UML序列圖與狀態圖進行了無縫銜接，不僅能夠對自適應環中的各個軟件實體交互關系進行刻畫，而且能夠對特定周期內單個軟件實體的活躍狀態進行準確描述，與此同時在形式化定義作用下，其能夠實現向時間自動機模型的有效轉化，進而為軟件自適應形式化驗證奠定堅實的基礎。

4.3 基于UML擴展的軟件自適應建模原則

此次研究軟件自適應建立的本質為自適應環（監視、分析、規劃、執行）與不斷變化軟件的交互，因此必須將參與自適應過程的軟件實體及自適應環作為一階要素給予顯示化建模與刻畫。其次，要遵循自適應邏輯外置分離原則，一般可采用外置式方式，從目標軟件系統中對自適應邏輯進行分離，這能夠在一定程度上避免應用邏輯與自適應邏輯之間的交織。除此之外，還必須遵循約束條件規范描述原則，對時間約束與事件約束進行相應的規范，其能夠為軟件自適應UML模型轉換奠定基礎。

5 軟件自適應模型轉換與形式化驗證（Software

adaptive model transformation and formal

verification）

5.1 軟件自適應UMI模型向時間自動機模型的轉換

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

5.2 軟件自適應形式化驗證

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

特殊變化時的應對情況。（4）自適應快速反應能力。其主要指的是觸發自適應行為后，自適應邏輯單元在一定時間內的響應速度與響應能力，其需要確保自適應策略的正確性與有效性。除此之外，還需要對軟件自適應行為進行模擬與形式化驗證。UPPAAL所提供的simulator模擬器能夠對軟件自適應交互過程進行模擬，并形成一個完整的運行軌跡，若運行出現錯誤，系統將會立即做出反饋，便于建模人員及時做出相關調整。在UPPAAL驗證器verifier中輸入TCTL可靠性規約，系統能夠對軟件自適應性質進行自動檢測，最終得到完善的軟件自適應模型。

6 結論（Conclusion）

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

參考文獻（References）

[1] 趙曉宇，等.基于HUML的列控系統形式化建模與參數分析方法[J].鐵道學報，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類圖形式化及驗證[J].云南民族大學學報自然科學版，2015，22（6）：506-509.

[5] 安越，李國寧.基于Timed-UML順序圖的RBC交接形式化建模與分析[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] 劉懷玉，陽西述，何昭青.算術四則運算智能測試教學軟件的設計[J].軟件工程師，2014，13（6）：42-43.

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

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

作者簡介：

施柏銓（1981-），男，本科，講師.研究領域：計算機科學與技

術學，計算機網絡.