一個局部性的並行正確性驗證工具─使用模型架構重置解構使用抽象化資料結構之行程行為

Abstract

模型檢測(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技術。Model Checking techniques have improved considerably in past decades. In practice, there are some difficulties to apply model checking technology to software, particularly to source code directly. Not only software has more states, but also it is not easy to narrow the gap between an implementation and its model. One of the problems is how to deal with the abstract data type in source code. In this thesis we present examples to show different modeling choices can result in great differences in analysis when process behaviors are complicated by array data type. In other words, software verification is very sensitive to modeling choices. To lessen the sensitivity, we advocated the support of abstract data types in model description languages and suppressing the use of array. Encouraging the use of abstract data types can lessen the sensitivity of analysis to modeling choices and converge the process behaviors to their best for analysis. In this work, we implement a tool named COCOV (Compositional Concurrency Verifier) supports abstract data types. We show that analysis (particularly, compositional analysis and our refactoring technique) can benefit from this tool support in an obvious way.