Browsing by Author "Zhi-Wen Hsu"

Filter results by typing the first few letters
Now showing 1 - 1 of 1
  • No Thumbnail Available
    Item
    ArCats局部性模型分析安全性質和活化性質
    (2006) 徐志文; Zhi-Wen Hsu
    近年來，局部性模型分析在自動化軟體驗證領域中佔有一席角色。局部性模型分析能夠成功的關鍵在於檢驗的系統模型具有良好的階層架構，同時盡量利用最小化的技術減化子系統的內部行為，達到減緩組態爆炸的發生。透過模型架構重構可以解決不良的模型架構，這增強局部性分析的效能。當利用局部性分析檢驗系統性質時，因為保留過多的系統性質到全域系統中，造成子系統無法最小化的結果，這將大幅消減局部性分析在模型驗證中的效能。 在本篇論文中，我們根據ArCats和其在局部性分析中所提供的良好功能，開發出能夠檢測系統安全性質(safety)和活化性質(liveness)的功能，同時並能夠維持局部性分析的減緩狀態爆炸的優勢。在檢驗安全性質時，我們利用一種類似死結狀態的π狀態，讓違反安全性的系統行為能夠被偵測出來。而在檢驗活化性質時我們使用一種特殊的接受轉移（accept transition）來代表系統符合檢驗性質。這兩種在局部性分析中檢測性質，主要參考Cheung[28][29][30]的研究。但是由於ArCats是以CCS為基礎來提供模型架構重構的功能而Cheung的研究採用的是CSP，本篇論文將針對如何利用以CSP為基礎的驗證技術實做到以CCS為基礎的驗證工具中，同時探討與解決所面臨的困難。