[erlang-questions] Model Checking (was: Re: erlang-questions Digest, Vol 12, Issue 102)

[Mathias Dalheimer]

Hi,

On May 31, 2008, at 12:44 AM, Raoul Duke wrote:

> hi,
>
>> With respect to avoiding deadlocks or ensuring there are none, I  
>> would
>> 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  
useful.

 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) 
.

HTH,
-Mathias
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3596 bytes
Desc: not available
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20080531/6e147e05/attachment.bin>