Erlang and Model Checker "Spin"
Thu Jul 12 11:12:26 CEST 2001
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.
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
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:
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
Computer Science Lab
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 6700 bytes
Desc: not available
More information about the erlang-questions