針對硬體的驗證工作，模型檢驗(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.