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