|
|
| Author |
Message |
|
| kramer at acm.org |
 Posted: Wed Jul 11, 2001 5:58 am |
 |
|
|
Guest
|
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.
cheers,
- Reto
Post generated using Mail2Forum (http://m2f.sourceforge.net) |
|
|
| Back to top |
|
| thomas at cslab.ericsson. |
| Posted: Thu Jul 12, 2001 9:12 am |
|
|
|
Guest
|
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/
Post generated using Mail2Forum (http://m2f.sourceforge.net) |
|
|
| Back to top |
|
|
|
All times are GMT
|
|
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You cannot attach files in this forum
You cannot download files in this forum
|
|
|
Digg It
Del.icio.us
Reddit
Facebook
Stumble Upon
Technorati
