|
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.
|