I've used it several times but the big problem with it is that once you have a nice, correct model that has been checked (and no counterexamples found), there's no way to translate it to code. This meand that your basically back on square one in terms of implementation.

I really like (and use quite often) the ASM method instead.

More of my thoughts here: http://ortask.com/how-i-designed-built-and-tested-a-temperat...