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