On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP

Hubert Garavel 1 Gwen Salaun 1 Wendelin Serwe 1, *
* Auteur correspondant
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Hardware process calculi, such as CHP (Communicating Hardware Processes), Balsa, or Haste (formerly Tangram), are a natural approach for the description of asynchronous hardware architectures. These calculi are extensions of standard process calculi with particular synchronisation features implemented using handshake protocols. In this article, we first give a structural operational semantics for value-passing CHP. Compared to the existing semantics of CHP defined by translation into Petri nets, our semantics is general enough to handle value-passing CHP with communication channels open to the environment, and is also independent of any particular (2- or 4-phase) handshake protocol used for circuit implementation. We then describe the translation of CHP into the process calculus LOTOS (ISO standard 8807), in order to allow asynchronous hardware architectures expressed in CHP to be verified using the CADP verification toolbox for LOTOS. A translator from CHP to LOTOS has been implemented and successfully used for the compositional verification of two industrial case studies, namely an asynchronous implementation of the DES (Data Encryption Standard) and an asynchronous interconnect of a NoC (Network on Chip).
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2009
Liste complète des métadonnées

Littérature citée [44 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00381642
Contributeur : Wendelin Serwe <>
Soumis le : mercredi 6 mai 2009 - 11:13:49
Dernière modification le : mercredi 11 avril 2018 - 01:55:23
Document(s) archivé(s) le : jeudi 10 juin 2010 - 19:53:07

Fichier

Garavel-Salaun-Serwe-09.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00381642, version 1

Citation

Hubert Garavel, Gwen Salaun, Wendelin Serwe. On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP. Science of Computer Programming, Elsevier, 2009. 〈inria-00381642〉

Partager

Métriques

Consultations de la notice

309

Téléchargements de fichiers

236