請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/3788
標題: | 利用時態分解技術增進性質導向可達性技術 Improving Property Directed Reachability with Temporal Decomposition |
作者: | Ming-Jen Yang 楊明仁 |
指導教授: | 黃鐘揚(Chung-Yang (Ric) |
關鍵字: | 驗證,正規驗證,性質導向可達性,時態分解, Verification,Formal Verification,PDR,Temporal Decomposition, |
出版年 : | 2016 |
學位: | 碩士 |
摘要: | 因為對於安全或是不安全的案例都有突出的效能,性質導向可達性技術從二零一一年發表以來一直是模式驗證問題中最有效率的演算法。然而,因為模式驗證問題本質上的高複雜度,還是有許多的案例沒有被驗證。因此,改善性質導向可達性技術的研究是一個非常重要的主題,近來也產生了許多相關的研究。在這篇論文中,我們提出了三種基於將時態分解技術的概念融合於性質導向可達性技術的創新方法。我們將我們所提出的方法實作於“驗證三”的驗證架構中,並且使用世界”硬體模式驗證競賽”的案例與原本的性質導向可達性技術做比較。實驗結果顯示我們的方法可以驗證許多原本未被驗證的案例,對不安全的案例有一點四倍的運作時間提升,代表著這些方法可以與原本的性質導向可達性技術在相當多的基準點上互補。 Property Directed Reachability has always been the most efficient algorithm for the safety property checking problem for its well performance on both safe and unsafe case since its publication in 2011. However, there are still a large number of cases remaining unsolved due to the intrinsic high complexity of model checking problem. Therefore, improving PDR is an important subject and attracts lots of research recently. In this paper, we present three novel approaches that integrate a sequential optimization technique, called temporal decomposition into PDR. We implemented our work in V3 and compared to original PDR in V3 on HWMCC benchmarks. The experimental result shows that the proposed methods solved many originally unsolved cases, and improved unsafe cases by 1.4x in runtimes. It means that these methods can complement original PDR on a large set of benchmarks. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/3788 |
DOI: | 10.6342/NTU201601674 |
全文授權: | 同意授權(全球公開) |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-105-1.pdf | 2.77 MB | Adobe PDF | 檢視/開啟 |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。