Links

Tools

Export citation

Search in Google Scholar

Experiments in Translating CSP parallel to B to Handel-C

Proceedings article published in 2008 by Steve Schneider, Helen Treharne, Alistair McEwan, Wilson Ifill
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Question mark in circle
Preprint: policy unknown
Question mark in circle
Postprint: policy unknown
Question mark in circle
Published version: policy unknown

Abstract

This paper considers the issues involved in translating specifications de- scribed in the CSPkB formal method into Handel-C. There have previously been ap- proaches to translating CSP descriptions to Handel-C, and the work presented in this paper is part of a programme of work to extend it to include the B component of a CSPkB description. Handel-C is a suitable target language because of its capability of programming communication and state, and its compilation route to hardware. The paper presents two case studies that investigate aspects of the translation: a buffer case study, and an abstract arbiter case study. These investigations have exposed a number of issues relating to the translation of the B component, and have identified a range of options available, informing more recent work on the development of a style for CSPkB specifications particularly appropriate to translation to Handel-C.