基于時間屬性序列圖的運行驗證技術(shù)研究.pdf

1、隨著信息技術(shù)的發(fā)展，計算機技術(shù)已經(jīng)融入了現(xiàn)代社會各個領(lǐng)域，得到極其廣泛的應(yīng)用。然而在這樣的背景下，計算機系統(tǒng)的異?？赡軙斐蔀?zāi)難性后果。
　　測試和仿真通常被用來保障這類安全關(guān)鍵系統(tǒng)的可靠性，但是這類方法針對的是實際運行前的系統(tǒng)，只能檢測到系統(tǒng)的錯誤，而不能證明系統(tǒng)的正確。模型驗證是完備的，但是它針對的是系統(tǒng)的抽象模型，難以證明系統(tǒng)的抽象模型和實際系統(tǒng)的等價性，同時這種方法需要遍歷系統(tǒng)的所有執(zhí)行路徑，對于復(fù)雜系統(tǒng)來說，容易產(chǎn)生組合

2、爆炸問題。
　　與傳統(tǒng)的測試和模型驗證技術(shù)不同，運行時驗證針對的是正在運行的實際系統(tǒng)。運行時驗證一般采用時態(tài)邏輯來描述要驗證的需求規(guī)約，并根據(jù)需求規(guī)約構(gòu)造監(jiān)控器。利用UML序列圖來描述要驗證的需求規(guī)約，克服了時態(tài)邏輯等形式化方法使用復(fù)雜的問題，使得普通的軟件工程師也能方便正確的描述要驗證的需求規(guī)約或性質(zhì)。研究基于時間屬性序列圖(TPSD，Timed Property Sequence Diagram)自動生成監(jiān)控器來進行運行時驗證

3、就顯得十分有意義。
　　本文提出了基于UML2.0時間屬性序列圖的運行時驗證方法，其具體思想是使用時間屬性序列圖來描述要驗證的需求規(guī)約，然后為序列圖中的每個對象構(gòu)造時間對象自動機，將整個序列圖轉(zhuǎn)換為時間自動機網(wǎng)絡(luò)，以構(gòu)造出運行時驗證中所需的監(jiān)控器，監(jiān)控器監(jiān)控目標系統(tǒng)的執(zhí)行軌跡，判斷目標系統(tǒng)的當前執(zhí)行是否滿足需求規(guī)約。本文先給出了滿足本文驗證需求的時間屬性序列圖形式化定義，接著提出了時間對象自動機及其形式化定義，然后提出了基于時間屬

4、性序列圖的運行時驗證方法的基本原理，進而提出了將時間屬性序列圖轉(zhuǎn)化為時間自動機網(wǎng)絡(luò)來構(gòu)造預(yù)測監(jiān)控器的算法。在此基礎(chǔ)上，本文利用上述原理構(gòu)造了一個基于時間屬性序列圖的運行時驗證工具TPSD_monitor，構(gòu)造了一個列控系統(tǒng)CTCS-2向CTCS-3級間切換仿真程序作為要驗證的目標系統(tǒng)，利用該工具對構(gòu)造的目標系統(tǒng)進行運行時驗證，說明了本文中方法對安全關(guān)鍵系統(tǒng)進行運行時驗證的可行性。進而進行了性能對比試驗，實驗表明，本文的監(jiān)控器構(gòu)造方法所產(chǎn)