Yes, SPIN is a very good model, but I wonder what you want? Do you just want to hear that, yes, I heard and played with SPIN, or do you need suggestions for modeling the verification source code?
For example, if you are a C programmer, hold ESBMC hands, write a small program, and start ESBMC.
This should make you understand what can be done and how to do it. By the way, for starters Model Checking is not a static analysis. It is actually much more powerful. This is an antistatic analysis. Testing the model actually "in a very narrow sense" simulates your program and finds situations (combinations of arguments, exceptions, border cases) where it really fails.