|
|
|
|
|
Spin Model CheckerSpin is a tool for software model checking. It was written by Gerard J. Holzmann and others, and has evolved for more than 15 years. Spin is a automata-based model checker, as it represents the negated LTL property it checks the model against by a Bchi automaton. It then performs a depth-first search for the recurrent reachability of an accepting state of the product automaton. If there exists some path that reaches this accepting state infinitely often, it serves as a counterexample. Spin offers a large amount of options to speed up the checking process and save memory, like Spin does not perform the model checking itself but generates C sources for a problem-specific model checker. This rather antique technique saves memory and speeds things up, and also allows to directly insert chunks of C code into the model. External links Spin home page
|
 |
|
| Copyright 2005-2009 OnPedia.com. All Rights Reserved |
|
|