Sciweavers

Share
IFM
2007
Springer

Translating FSP into LOTOS and Networks of Automata

10 years 5 months ago
Translating FSP into LOTOS and Networks of Automata
Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. Fsp is a widely-used calculus equipped with Ltsa, a graphical and user-friendly tool. Lotos is the only process calculus that has led to an international standard, and is supported by the Cadp verification toolbox. We propose a translation from Fsp to Lotos. Since Fsp composite processes are hard to encode into Lotos, they are translated into networks of automata which are another input language accepted by Cadp. Hence, it is possible to use jointly Ltsa and Cadp to validate Fsp specifications. Our approach is completely automated by a translator tool we implemented.
Gwen Salaün, Jeff Kramer, Frédé
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where IFM
Authors Gwen Salaün, Jeff Kramer, Frédéric Lang, Jeff Magee
Comments (0)
books