學位論文

Permanent URI for this collectionhttp://rportal.lib.ntnu.edu.tw/handle/20.500.12235/73881

Browse

Filter results by typing the first few letters
Now showing 1 - 1 of 1
  • No Thumbnail Available
    Item
    一個局部性的並行正確性驗證工具─使用模型架構重置解構使用抽象化資料結構之行程行為
    (2004) 吳克仁; Keh-Ren Wu
    模型檢測(model checking)技術在最近幾年發展越來越成熟，然而在實際上不容易將這技術應用在軟體，特別是要直接從原始碼抽出模型，原因在於軟體會產生的狀態(state)多於硬體。此外，要如何確保從模型到實作的差距也是個困難的議題。 本篇論文中，我們使用幾個例子來說明：當一個程序(process)含有複雜的陣列(array)行為時「模型的實作選擇會造成在分析時有很大的影響」。換句話說，軟體驗證(software verification)的結果跟模型的實作選擇有很大的關係。為了減少模型實作選擇的影響力，我們建議在模型描述語言(model description language)提供抽象的資料型別(abstract data type)，並且避免使用讓使用者用陣列來實作這些抽象資料型別。鼓勵使用這些抽象資料型別除了可以減少在驗證時模型實作選擇的影響力，我們也可以使用作適合該資料型別的分析方式。 我們實作了COCOV(Compositional Concurrency Verifier)，以rc-Promela(修改自Promela，Promela是驗證工具SPIN的模型描述語言)為基礎並且讓COCOV支援了set、queue的抽象資料型別，並說明如何透過該工具讓我們可以在分析時獲得明顯的幫助，尤其是在局部性分析(compositional analysis)與我們的refactoring技術。