基于運行時驗證的監(jiān)控器優(yōu)化方法研究
發(fā)布時間：2021-10-07 16:16
隨著計算機軟件系統(tǒng)規(guī)模的不斷擴大和復雜性的逐漸增加,驗證軟件系統(tǒng)正確性和可靠性的難度也越來越大,傳統(tǒng)的驗證技術(shù)已經(jīng)無法滿足需求。運行時驗證是一種提高軟件系統(tǒng)正確性和可靠性的輕量級驗證技術(shù),是傳統(tǒng)驗證技術(shù)的有效補充,它通過監(jiān)控軟件系統(tǒng)的實際運行狀態(tài)來驗證軟件系統(tǒng)是否正確。然而,在運行時驗證中,監(jiān)控軟件系統(tǒng)的運行狀態(tài)通常會產(chǎn)生一些額外的運行時開銷,這會對軟件系統(tǒng)的性能造成一定的影響。因此,減少運行時驗證的開銷是運行時驗證領(lǐng)域中一個重要的研究內(nèi)容。本文圍繞如何有效地減少運行時驗證的開銷問題進行研究,具體對運行時驗證工具JavaMOP展開研究工作。對JavaMOP進行優(yōu)化,降低JavaMOP運行時驗證的時間和內(nèi)存開銷,提高運行時驗證工具JavaMOP的驗證效率。本文首先分析JavaMOP驗證線性時態(tài)邏輯（Linear Temporal Logic,LTL）性質(zhì)時監(jiān)控器的構(gòu)造過程,研究并提出了一種改進的監(jiān)控器構(gòu)造方法。該方法使用基于遷移的廣義Büchi自動機（Transition-based Generalized Büchi Automaton,TGBA）作為中間的輔助自動機。將LTL性質(zhì)直接...
【文章來源】：桂林電子科技大學廣西壯族自治區(qū)
【文章頁數(shù)】：53 頁
【學位級別】：碩士
【部分圖文】：
基于監(jiān)控器的系統(tǒng)驗證過程
基于運行時驗證的監(jiān)控器優(yōu)化方法研究證；監(jiān)控器與目標系統(tǒng)不同時運行的驗證即為離線驗證也稱為脫機驗證，主要是對標系統(tǒng)的歷史記錄進行分析，排查和修復系統(tǒng)故障。§2.2.3 JavaMOP面向監(jiān)控編程（MOP）是一種用于軟件開發(fā)和分析的形式化框架，很多運行驗證是在該框架下完成的。在該框架中，使用形式化規(guī)范來指定需要的系統(tǒng)行為屬性指定的屬性自動生成監(jiān)控器，并集成到目標系統(tǒng)中，驗證系統(tǒng)程序的運行狀態(tài)。當統(tǒng)在運行時違反某個屬性時，將觸發(fā)用戶定義的操作，給出反饋信息。圖 2-2 是面監(jiān)控編程框架的分層體系結(jié)構(gòu)。頂層是接口層，為用戶提供編程環(huán)境；第二層中規(guī)處理器用于處理監(jiān)控器集成；第三、四層包含邏輯插件，由第三層的語言腳本和第層的邏輯引擎組成，用戶可以進行添加、刪除和修改等操作。
圖 2-3 面向監(jiān)控編程框架的監(jiān)控模型JavaMOP 是一種基于面向監(jiān)控編程框架的 Java 軟件開發(fā)與分析環(huán)境，是面向編程框架的一個實例，繼承了面向監(jiān)控編程框架的體系結(jié)構(gòu)。JavaMOP 是一種的運行時驗證工具，它為編輯和處理規(guī)范提供了 GUI 和命令行接口，支持多種形式的邏輯規(guī)范，將處理各種形式化邏輯規(guī)范語言的算法以邏輯插件的形式集成avaMOP 運行時驗證工具中，如：LTL 插件、ERE 插件、FSM 插件和 CFG 插件等后根據(jù)給定系統(tǒng)行為屬性的邏輯規(guī)范語言，調(diào)用對應的插件進行監(jiān)控系統(tǒng)運行的。另外，JavaMOP 還支持參數(shù)化系統(tǒng)監(jiān)控[19]，因為它支持多種形式化規(guī)范，在化監(jiān)控上完全不受邏輯規(guī)范形式的限制。使用 JavaMOP 對系統(tǒng)進行運行時驗證，首先根據(jù)需要選擇合適的形式化邏輯描述系統(tǒng)行為屬性，采用 mop 語法編輯生成 mop 格式的文檔；然后 JavaMOP 將行為的屬性規(guī)范轉(zhuǎn)化生成用于監(jiān)控系統(tǒng)運行情況的 AspectJ 監(jiān)控代碼；再由 Aspe譯器[56]將 AspectJ 監(jiān)控代碼插裝到目標程序中。圖 2-4 即為 JavaMOP 運行時驗證程序的過程。在系統(tǒng)運行時驗證中，生成的監(jiān)控器代碼觀察系統(tǒng)運行的程序，捕屬性規(guī)范定義的事件，并檢查系統(tǒng)程序的運行是否符合給定的屬性規(guī)范。當出現(xiàn)
【參考文獻】：
期刊論文
[1]運行時驗證中的減少監(jiān)控開銷方法研究[J]. 徐勝,葉俊民,陳曙,金聰,陳盼. 計算機科學. 2016(05)
[2]運行時驗證及其在列車運行控制系統(tǒng)中的應用[J]. 趙林,唐濤,徐田華,柴銘,李憲. 鐵道學報. 2011(12)
[3]基于AOP的運行時驗證中的沖突檢測[J]. 張獻,董威,齊治昌. 軟件學報. 2011(06)
本文編號：3422371
【文章來源】：桂林電子科技大學廣西壯族自治區(qū)
【文章頁數(shù)】：53 頁
【學位級別】：碩士
【部分圖文】：
基于監(jiān)控器的系統(tǒng)驗證過程
基于運行時驗證的監(jiān)控器優(yōu)化方法研究證；監(jiān)控器與目標系統(tǒng)不同時運行的驗證即為離線驗證也稱為脫機驗證，主要是對標系統(tǒng)的歷史記錄進行分析，排查和修復系統(tǒng)故障。§2.2.3 JavaMOP面向監(jiān)控編程（MOP）是一種用于軟件開發(fā)和分析的形式化框架，很多運行驗證是在該框架下完成的。在該框架中，使用形式化規(guī)范來指定需要的系統(tǒng)行為屬性指定的屬性自動生成監(jiān)控器，并集成到目標系統(tǒng)中，驗證系統(tǒng)程序的運行狀態(tài)。當統(tǒng)在運行時違反某個屬性時，將觸發(fā)用戶定義的操作，給出反饋信息。圖 2-2 是面監(jiān)控編程框架的分層體系結(jié)構(gòu)。頂層是接口層，為用戶提供編程環(huán)境；第二層中規(guī)處理器用于處理監(jiān)控器集成；第三、四層包含邏輯插件，由第三層的語言腳本和第層的邏輯引擎組成，用戶可以進行添加、刪除和修改等操作。
圖 2-3 面向監(jiān)控編程框架的監(jiān)控模型JavaMOP 是一種基于面向監(jiān)控編程框架的 Java 軟件開發(fā)與分析環(huán)境，是面向編程框架的一個實例，繼承了面向監(jiān)控編程框架的體系結(jié)構(gòu)。JavaMOP 是一種的運行時驗證工具，它為編輯和處理規(guī)范提供了 GUI 和命令行接口，支持多種形式的邏輯規(guī)范，將處理各種形式化邏輯規(guī)范語言的算法以邏輯插件的形式集成avaMOP 運行時驗證工具中，如：LTL 插件、ERE 插件、FSM 插件和 CFG 插件等后根據(jù)給定系統(tǒng)行為屬性的邏輯規(guī)范語言，調(diào)用對應的插件進行監(jiān)控系統(tǒng)運行的。另外，JavaMOP 還支持參數(shù)化系統(tǒng)監(jiān)控[19]，因為它支持多種形式化規(guī)范，在化監(jiān)控上完全不受邏輯規(guī)范形式的限制。使用 JavaMOP 對系統(tǒng)進行運行時驗證，首先根據(jù)需要選擇合適的形式化邏輯描述系統(tǒng)行為屬性，采用 mop 語法編輯生成 mop 格式的文檔；然后 JavaMOP 將行為的屬性規(guī)范轉(zhuǎn)化生成用于監(jiān)控系統(tǒng)運行情況的 AspectJ 監(jiān)控代碼；再由 Aspe譯器[56]將 AspectJ 監(jiān)控代碼插裝到目標程序中。圖 2-4 即為 JavaMOP 運行時驗證程序的過程。在系統(tǒng)運行時驗證中，生成的監(jiān)控器代碼觀察系統(tǒng)運行的程序，捕屬性規(guī)范定義的事件，并檢查系統(tǒng)程序的運行是否符合給定的屬性規(guī)范。當出現(xiàn)
【參考文獻】：
期刊論文
[1]運行時驗證中的減少監(jiān)控開銷方法研究[J]. 徐勝,葉俊民,陳曙,金聰,陳盼. 計算機科學. 2016(05)
[2]運行時驗證及其在列車運行控制系統(tǒng)中的應用[J]. 趙林,唐濤,徐田華,柴銘,李憲. 鐵道學報. 2011(12)
[3]基于AOP的運行時驗證中的沖突檢測[J]. 張獻,董威,齊治昌. 軟件學報. 2011(06)
本文編號：3422371
本文鏈接：http://sikaile.net/kejilunwen/ruanjiangongchenglunwen/3422371.html
最近更新
教材專著
