Translating FSP into LOTOS and Networks of Automata

Frédéric Lang; Gwen Salaün; Rémi Hérilier; Jeff Kramer; Jeff Magee

hal-00533808, version 1

Translating FSP into LOTOS and Networks of Automata

Frédéric Lang ¹, Gwen Salaün ^1, 2, Rémi Hérilier ¹, Jeff Kramer ³, Jeff Magee ³

Formal Aspects of Computing 22 (2010) 681-711

Abstract: 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 possiblethe 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 of FSP sequential processes into Lotos. Since FSP composite processes (i.e., parallel compositions of processes) are hard to encode directly in 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.

1: VASY (INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble)
INRIA – Institut polytechnique de Grenoble (Grenoble INP) – Université Joseph Fourier - Grenoble I – Université Pierre-Mendès-France - Grenoble II – CNRS : UMR5217
2: Institut Polytechnique de Grenoble (Grenoble INP)
Institut National Polytechnique de Grenoble (INPG)
3: Department of Computing, Imperial College London
Imperial College London

hal-00533808, version 1
http://hal.archives-ouvertes.fr/hal-00533808
oai:hal.archives-ouvertes.fr:hal-00533808
From: Christine Mckinty <>
Submitted on: Monday, 8 November 2010 13:06:04
Updated on: Thursday, 9 December 2010 16:14:05

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="article"><head>Articles in peer-reviewed journal</head>
<biblStruct type="article" xml:id="hal-00533808"><analytic>
<author><persName><forename>Frédéric</forename><surname>Lang</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble</orgName>
<orgName type="team">VASY</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut polytechnique de Grenoble (Grenoble INP)</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Université Pierre-Mendès-France - Grenoble II</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
</affiliation>
</author>
<author><persName><forename>Gwen</forename><surname>Salaün</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble</orgName>
<orgName type="team">VASY</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut polytechnique de Grenoble (Grenoble INP)</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Université Pierre-Mendès-France - Grenoble II</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">Grenoble INP</orgName>
<orgName type="team">Institut Polytechnique de Grenoble</orgName>
<country>FR</country>
<orgName type="institution">Institut National Polytechnique de Grenoble (INPG)</orgName>
</affiliation>
</author>
<author><persName><forename>Rémi</forename><surname>Hérilier</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble</orgName>
<orgName type="team">VASY</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut polytechnique de Grenoble (Grenoble INP)</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Université Pierre-Mendès-France - Grenoble II</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
</affiliation>
</author>
<author><persName><forename>Jeff</forename><surname>Kramer</surname></persName>
<affiliation>
<orgName type="team">Department of Computing, Imperial College London</orgName>
<country>GB</country>
<orgName type="institution">Imperial College London</orgName>
</affiliation>
</author>
<author><persName><forename>Jeff</forename><surname>Magee</surname></persName>
<affiliation>
<orgName type="team">Department of Computing, Imperial College London</orgName>
<country>GB</country>
<orgName type="institution">Imperial College London</orgName>
</affiliation>
</author>
<title type="main" level="a">Translating FSP into LOTOS and Networks of Automata</title></analytic><monogr><title level="j" type="main">Formal Aspects of Computing</title><imprint><biblScope type="publicationDate">2010-11-00</biblScope><biblScope type="vol">22</biblScope><biblScope type="pp">681-711</biblScope></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00533808</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00533808/PDF/Lang-Salaun-Herilier-Kramer-Magee-version-HAL.pdf</idno></biblStruct>
</listBibl>
</listBibl>