Test and Verification of Concurrent Programs Using the Model Checker SPIN

• Main Authors: Chu, Liang-Jung, 朱良鈞
• Other Authors: Ting-Lu Huang
• Format: Others
• Language: zh-TW
• Published: 1998
• Online Access: http://ndltd.ncl.edu.tw/handle/09094884337750961202

碩士 === 國立交通大學 === 資訊工程學系 === 86 === 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.