使用模型檢驗器SPIN測試與驗證並行程式

Abstract

針對硬體的驗證工作，模型檢驗(model checking)已被證明是一項十 分成功的技術。我們以實例說明如何使用模型檢驗器(model checker) SPIN測試與驗證並行程式(concurrent program)。首先，我們使用SPIN尋 找出兩個已刊載的互斥程式(mutual exclusion algorithm)的錯誤。將這 種傑出的找錯能力應用到情節方法(scenario approach)上，對於程式， 我們將獲得更多有關各組成要素的了解。接著，我們使用SPIN協助發展並 行程式。模型檢驗中的主要難題稱為狀態劇增問題(state explosion problem)。我們所提出用以解決狀態劇增的方法，是利用SPIN的特性以及 對目標程式所擁有的知識。最後，根據我們的試驗，我們要鼓勵軟體設計 者使用模型檢驗器，將它視為偵錯及驗證工作的輔助工具。 Model checking is a proven successful technology for verifying hardware. We demonstrate how model checking can be used to test and verify concurrent programs with the model checker SPIN. First, we use SPIN to find subtle errors in two published mutual exclusion algorithms. By applying this outstanding capability of finding errors to a scenario approach, we would gain a component-wise understanding of the target program. Then, we use SPIN to help develop concurrent programs. The main problem in model checking is the state explosion problem. Our approach to attacking state explosion exploits the nature of SPIN and the knowledge of the target program. Finally, according to our experiment we intend to encourage software designers to use a model checker as a tool in both debugging and verification.