On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP

DOI10.1016/j.scico.2008.09.011zbMath1160.68465OpenAlexW2075272319MaRDI QIDQ1001805

Wendelin Serwe, Hubert Garavel, Gwen Salaün

Publication date: 19 February 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00381642/file/Garavel-Salaun-Serwe-09.pdf

zbMATH Keywords

verificationmodellingstructured operational semanticstranslationspecificationvalidationasynchronyprocess calculusformal methodhardware designasynchronous circuitnetwork on chiphardware architectureasynchronous logicchpgals architecturehandshake protocollotos

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computer system organization (68M99)

Related Items (3)

Revisiting sequential composition in process calculi ⋮ CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes ⋮ Compositional verification of asynchronous concurrent systems using CADP

Uses Software

• BISIMULATOR
• M-TREE
• LOTOS
• CADP
• CAESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• State space reduction for process algebra specifications
• Modelling and verification of delay-insensitive circuits using CCS and the concurrency workbench
• The probe: An addition to communication primitives
• Compiling communicating processes into delay-insensitive VLSI circuits
• A calculus of communicating systems
• An exercise in the automatic verification of asynchronous designs
• Handshake Circuits
• Balsa: An Asynchronous Hardware Synthesis Language
• Translating Hardware Process Algebras into Standard Process Algebras: Illustration with CHP and LOTOS
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP