[erlang-questions] Model Checking (was: Re: erlang-questions Digest, Vol 12, Issue 102)
Sat May 31 08:57:39 CEST 2008
On May 31, 2008, at 12:44 AM, Raoul Duke wrote:
>> With respect to avoiding deadlocks or ensuring there are none, I
>> design my system based on CSP (Communicating sequential processes)
>> concepts. i.e Independent processes communicating via a pipe without
>> any shared memory.
> I believe that's sort of what Erlang does by nature ;-) so it is then
> a question of what modeling tools exist and how well they work. It
> isn't enough to design with CSP, you can still create deadlocks in it
> - you have to run a checker over it to try to prove there isn't any.
I recently used Spin to verify several models of distributed systems.
Spin follows the CSP paradigm - basically, you specify processes
communicating over pipes. The model gets translated into a C program
which is executed - Spin is highly optimized, although pretty memory
intensive. Spin is not directly related to Erlang, but still highly
From a methodological point of view you can design your protocol (and
the state machines) more or less interactively within Spin. After
you've implemented some functionality, you can "compile" the model and
run a verification. Spin provides builtin checks for deadlocks,
livelocks as well as over-/underspecification of code. In addition,
you can use linear temporal logic to specify your own properties.
Xspin (an X-Windows frontend) can display the sequence of actions that
violate any properties - so it's pretty easy to fix any problems.
In practice, I use Spin as the first step in distributed design and I
can really recommend it. You can get Spin from http://spinroot.com. If
you want to read more about it, "The Model Checker Spin" by Gerald
Holtzmann gives you a nice introduction (online at http://spinroot.com/spin/Doc/ieee97.pdf)
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 3596 bytes
Desc: not available
More information about the erlang-questions