本文關(guān)鍵詞：基于時間屬性序列圖的運行時驗證技術(shù)研究　出處：《華中師范大學》2014年碩士論文　論文類型：學位論文

  更多相關(guān)文章： 時間屬性序列圖 時間自動機 監(jiān)控器 運行時驗證

【摘要】：隨著信息技術(shù)的發(fā)展,計算機技術(shù)已經(jīng)融入了現(xiàn)代社會各個領(lǐng)域,得到極其廣泛的應用。然而在這樣的背景下,計算機系統(tǒng)的異�？赡軙斐蔀碾y性后果。 測試和仿真通常被用來保障這類安全關(guān)鍵系統(tǒng)的可靠性,但是這類方法針對的是實際運行前的系統(tǒng),只能檢測到系統(tǒng)的錯誤,而不能證明系統(tǒng)的正確。模型驗證是完備的,但是它針對的是系統(tǒng)的抽象模型,難以證明系統(tǒng)的抽象模型和實際系統(tǒng)的等價性,同時這種方法需要遍歷系統(tǒng)的所有執(zhí)行路徑,對于復雜系統(tǒng)來說,容易產(chǎn)生組合爆炸問題。 與傳統(tǒng)的測試和模型驗證技術(shù)不同,運行時驗證針對的是正在運行的實際系統(tǒng)。運行時驗證一般采用時態(tài)邏輯來描述要驗證的需求規(guī)約,并根據(jù)需求規(guī)約構(gòu)造監(jiān)控器。利用UML序列圖來描述要驗證的需求規(guī)約,克服了時態(tài)邏輯等形式化方法使用復雜的問題,使得普通的軟件工程師也能方便正確的描述要驗證的需求規(guī)約或性質(zhì)。研究基于時間屬性序列圖(TPSD, Timed Property Sequence Diagram)自動生成監(jiān)控器來進行運行時驗證就顯得十分有意義。 本文提出了基于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ī)約。本文先給出了滿足本文驗證需求的時間屬性序列圖形式化定義,接著提出了時間對象自動機及其形式化定義,然后提出了基于時間屬性序列圖的運行時驗證方法的基本原理,進而提出了將時間屬性序列圖轉(zhuǎn)化為時間自動機網(wǎng)絡(luò)來構(gòu)造預測監(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)生的監(jiān)控器運行開銷較小,且能在一定程度上緩解監(jiān)控器生成過程中的組合爆炸問題。
【學位授予單位】：華中師范大學
【學位級別】：碩士
【學位授予年份】：2014
【分類號】：TP306

【參考文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 曾光jf;;有限自動機基本模型及描述方法[J];電子技術(shù);1988年01期

2 梁冰;劉群;;基于時間自動機網(wǎng)的C~3I系統(tǒng)建模和實時性驗證[J];哈爾濱工程大學學報;2008年03期

3 孫玉強;劉三陽;王明斐;鄒凌;;有限狀態(tài)自動機的并行確定化及過程分析[J];計算機科學;2006年10期

4 周清雷,姬莉霞,王艷梅;基于UPPAAL的實時系統(tǒng)模型驗證[J];計算機應用;2004年09期

5 張亞紅;張琳琳;趙楷;陳佳麗;馮在文;;基于UML2.0序列圖的Web服務(wù)運行時驗證方法[J];計算機科學;2013年07期

6 柳毅;麻志毅;何嘯;邵維忠;;一種從UML模型到可靠性分析模型的轉(zhuǎn)換方法[J];軟件學報;2010年02期

7 趙常智;董威;隋平;齊治昌;;面向參數(shù)化LTL的預測監(jiān)控器構(gòu)造技術(shù)[J];軟件學報;2010年02期

8 張鵬程;李必信;李雯睿;;時間屬性序列圖:語法和語義[J];軟件學報;2010年11期

9 張琛;段振華;田聰;;基于事件確定有限自動機的UML2.0序列圖描述與驗證[J];軟件學報;2011年11期

10 張廣紅,陳平;關(guān)于AOP實現(xiàn)機制和應用的研究[J];計算機工程與設(shè)計;2003年08期

，

本文編號：1317778