|
|
| Author |
Message |
< Erlang ~ Erlang and Promela/Spin again |
| sv75 |
 Posted: Sun Jan 27, 2008 7:30 pm |
 |
|
|
User
Joined: 19 Oct 2007
Posts: 10
|
|
| Back to top |
  
|
| francesco |
| Posted: Mon Jan 28, 2008 8:27 am |
|
|
|
User
Joined: 07 Jul 2006
Posts: 249
Location: London
|
Thomas Arts will be in our offices in London today, presenting for the London Erlang User Group. This paper is one of many in this area. I;ll nudge Thomas so he gets back to you.
Francesco
--
http://www.erlang-consulting.com |
|
|
| Back to top |
|
| thomas |
| Posted: Mon Jan 28, 2008 9:33 am |
|
|
|
Joined: 13 Nov 2006
Posts: 7
Location: Göteborg
|
Yes, the paper should be somewhere, I'll look in my archive whether I can find it. Remind me if you don't hear from me in a week.
Promela got richer, thus probably nowadays one could do a good job with it. The problem back then was that translating the Erlang message queue in Promela was rather problematic. This has been improved in Promela, I know.
One rather big disadvantage, as I see it, is that the Promela code would have to be debugged/understood by Erlang programmers. Some of them will find this a happy task, others will be confused. The language mCRL is a bit closer to Erlang, but in the end, it is a disadvantage to translate.
McErlang, a new model checker for Erlang designed by Lars-Åke Fredlund et al, is a better alternative, since that takes the Erlang runtime system and modifies it into a model checker. In that way, you run your "normal" Erlang code on a different runtime system and as such you verify all possible runs. Simplisticly said, you automatically put a yield in almost any line of code and make sure you execute all possible runs of the program.
Regards
Thomas
|
|
|
| Back to top |
|
| sv75 |
| Posted: Mon Jan 28, 2008 3:16 pm |
|
|
|
User
Joined: 19 Oct 2007
Posts: 10
|
thomas wrote:
McErlang, a new model checker for Erlang designed by Lars-Åke Fredlund et al, is a better alternative, since that takes the Erlang runtime system and modifies it into a model checker.
Thomas, thank your for information, I'll check McErlang too. But I already gave a task about Promela/Erlang verification to one of my students so I'll be glad to read that report anyway. He'll use muCRL if Promela fails completely  |
|
|
| 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
Maybe somebody here knows current e-mail address of Thomas Arts?