Re: [moca] Model checking (Stochastic)pi-calculus

[Tom Chothia <tomc@xxxxxxxxxxxxxxxxxxx>]

As far as I'm aware there is no really good professional tool for
model checking pi-calculus. However, the "Edinburgh Concurrency
Workbench" (http://www.dcs.ed.ac.uk/home/cwb/summary.html) is worth a
look, although I think it only does CCS, rather than the full
pi-calculus.

Also interesting might be "The Mobility Workbench"
(http://www.it.uu.se/research/docs/fm/mobility/mwb) although I have not
used this one myself.

An alterative might be to use the Spin Model checker
(http://spinroot.com/spin/whatispin.html). Spin does not support the
pi-calculus exactly, but it does let you send channels over
channels. So, it could probably be made to work with very little
hacking.

Tom




On Mon, 19 May 2003, Pascal Poizat wrote:

> Hello,
>
> I am switching from CCS/CSP/LOTOS process algebras to pi-calculus
> (teaching & research).
> Do you know if there exist papers and/or tools on model-checking
> pi-calculus or stochastic pi-calculus ?
>
> Regards,
>
> Pascal
>
>
> --
> Pascal Poizat
> LaMI - UMR 8042 du CNRS / Universite d'Evry Val d'Essonne
> Tour Evry 2, 523 place des terrasses de l'Agora, 91000 EVRY, France
> http://www.lami.univ-evry.fr/~poizat
>
>
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
>  http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html
>
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html