請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/58542
標題: | 系統元件微調後之高效率模型驗證 Effective Model Checking for Component Adjusted Systems |
作者: | Yean-Ru Chen 陳盈如 |
指導教授: | 陳少傑(Sao-Jie Chen) |
關鍵字: | 正規驗證,模型驗證,定位,微調,修改,回歸,簡化,切割,遞增,部分模型驗證, formal verification,model checking,localization,adjustments,modifications,regression,reduction,slicing,incrementally partial model checking, |
出版年 : | 2014 |
學位: | 博士 |
摘要: | 模型驗證(model checking)用來驗證元件微調而改版後的大型系統,引起之狀
態空間爆增(state space explosion)的問題,會因為多次重覆驗證新版系統中的微調,而變得更加嚴重。我們在本篇論文中提出一個高效能的模型驗證架構,導入回歸測試(regression testing)的觀念,並且使得模型驗證在應用於多次重覆驗證新版系統,其狀態空間爆增的情況得到有效的改善。 我們提出的方法,包括了「非關鍵路徑切割法之模型驗證」(Non-critical Path Slicing Model Checking),以及「遞增式之部分模型驗證」(Incrementally Partial-Model Checking),並且與傳統的模型驗證,一併整合於名於「狀態圖運算器」(State Graph Manipulator, SGM)的模型驗證器中。 「非關鍵路徑切割法之模型驗證」與「遞增式之部分模型驗證」的理論,都 是基於相同的觀念:定位(localization)出與特性(properties)相關的微調之行為,並且僅重新驗證這些相關的行為,保證其驗證結果之正確性。 「非關鍵路徑切割法之模型驗證」,乃藉由刪除獨立於基本型特性(primitive properties independent)的狀態轉換,在系統狀態圖(system state graph)產生之前,就能減少驗證狀態的空間;而「遞增式之部分模型驗證」,則是藉由分析在新版系統中,哪一些狀態與結構型的微調(structural adjustments)有所相關,重新驗證這些具相關性的狀態。 本論文提供理論上的證明以確保驗證結果的正確性,並且將這些方法應用於 多個實際的硬體邏輯控制系統中。實驗數據顯示本方法,不論針對單一或多個特 性,驗證微調後的新版系統,都能夠提高模型驗證的執行效率。 To alleviate the state space explosion problem when model checking is applied on subsequent versions of a large system, an effective model checking framework is proposed in this Dissertation, which includes three verification procedures named Noncritical Path Slicing Model Checking (NPSMC), Incrementally Partial-Model Checking (IPMC), and Conventional Model Checking with State-space Reduction techniques (CMCSR). We adopt the localization principle and attempt to locate either the definitely unaffected behaviors or the possible affected behaviors, such that we can slice out the unaffected ones and correctly re-check only the affected ones. Thus unnecessary re-checking of a large portion of the system states is avoided and time is saved. The proposed framework has been integrated into the State Graph Manipulators model checker. Application examples show a dramatic improvement of up to 86.79%reduction in re-checking time and up to 76.68% reduction in memory usage for several component adjusted systems. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/58542 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-103-1.pdf 目前未授權公開取用 | 1.17 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。