Erlang and Model Checker "Spin"

[Thomas Arts]

Reto Kramer wrote:
> 
> I was wondering if anyone is aware of model checking work done in the
> context of Erlang.
> It seems that "Spin", the protocol model checker that Gerard Holzmann build
> at the Bell Labs allows for very relatively easy transformation from/to
> Erlang due to the similar communication models.
> 
> Any pointer to previous work in this area is greatly appreciated.

Dear Reto

We have experimented with a translation of Erlang into Promela
and checking Promela bij SPIN. This is reported upon in a
master thesis (http://www.ericsson.com/cslab/~thomas/Xjobb/christian.ps).
The main outcome of the experiment was that Promela (and hence SPIN)
are too far away from Erlang to really use them together. It is 
a little like using C to specify an Erlang program in.

We searched for a better specification language and found that in
mCRL, provided by CWI in Amsterdam (http://www.cwi.nl/~mcrl).
At first we used this language to manually specify Erlang programs in
and used the CADP model checker to verify properties 
(http://www.ericsson.com/cslab/~thomas/papers/ifl2000.pdf  and
 http://www.ericsson.com/cslab/~thomas/Reports/sen9910.ps).

The CADP toolset is really great and offers almost the same as SPIN
(http://www.inrialpes.fr/vasy/cadp). The user interface is very intuitive
and there are more features than we have used yet.

Using a specification language is always a little drawback, because it 
takes you lots of extra work. The work may pay of in the end, but often
it is just tedious, since the Erlang program can be seen as a specification
as well. We wrote a program to translate Erlang to mCRL for at least
a subset of Erlang large enough to look at an interesting case study:
http://www.ericsson.com/cslab/~thomas/papers/fmics2001.pdf)

I attached a few Erlang models to give you an impression on what we can verify
automatically by using model checking.

Please feel free to contact me for further questions
Thomas


---
Thomas Arts
Ericsson
Computer Science Lab

http://www.ericsson.com/cslab/~thomas/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: verifiedlocker-0.3.tgz
Type: application/octet-stream
Size: 6700 bytes
Desc: not available
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20010712/86275ca0/attachment.obj>