CHP2LOTOS Translator for CHP (Communicating Hardware Processes)

Organisation:	Inria Grenoble Rhône-Alpes and LIG, Grenoble (FRANCE)
Functionality:	Translation from CHP (Communicating Hardware Processes) into LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2005-2009
Description:	CHP (Communicating Hardware Processes) is a process calculus dedicated to the description of asynchronous hardware architectures. CHP extends standard process calculi with particular synchronisation features implemented using handshake protocols. The CHP2LOTOS tool translates a CHP description into LOTOS, enabling their verification with the CADP toolbox. The particular synchronisation features (e.g., the probe operator) are translated into dedicated processes to represent communication channels. Whenever possible, CHP2LOTOS optimises the translation avoiding channel processes. CHP2LOTOS is equipped with a generic C library to support the numerical data types of CHP.
Conclusions:	The CHP2LOTOS translator provides a direct connection of the CHP language for asynchronous hardware to all the state-of-the-art verification features of the CADP toolbox. The translator was validated in several case-studies, including a router of an asynchronous network on chip.
Publications:	[Garavel-Salaun-Serwe-09] Hubert Garavel, Gwen Salaün, and 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, volume 74, number 3, pages 100-127, January 2009. Available on-line at: http://hal.inria.fr/inria-00381642/en or from the CADP Web site in PDF or PostScript [Salaun-Serwe-05] Gwen Salaün and Wendelin Serwe. "Translating Hardware Process Algebras into Standard Process Algebras &emdash; Illustration with CHP and LOTOS". Proceedings of the 5th International Conference on Integrated Formal Methods IFM'2005 (Eindhoven, The Netherlands), volume 3771 of Lecture Notes in Computer Science, Springer Verlag, November 2005. Available on-line at: http://hal.inria.fr/inria-00070342/en or from the CADP Web site in PDF or PostScript
Contact:	Wendelin Serwe Inria Grenoble Rhône Alpes / VASY project-team 655, avenue de l'Europe 38330 Montbonnot FRANCE E-mail: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page