CSP/FDR2 to Handel-C translation

Susan Stepney

CSP/FDR2 to Handel-C translation

Computer Science

Research output: Book/Report › Other report

Abstract

This report is adapted from a study performed for AWE in 2001 by the author while at Logica. It investigates the feasibility of using the CSP specification language and FDR2 model-checking tool, and Handel-C programming language, in combination, with FDR2 as a front-end specification and proof tool, then automatically translating the formal designs into executable Handel-C. Such an approach could provide a development path from an abstract specification to a correct executable implementation running on an FPGA.

This report contains the following

a) Identification of a subset of CSP that maps closely to Handel-C. That subset is large enough to accommodate a large subset of CSP specifications.

b) A sketch of a mapping from the identified CSP subset to Handel-C, suitable to be performed automatically. As proof-of-concept, the identified mappings are hand-applied to two example CSP specifications to produce Handel-C implementations.

Original language	Undefined/Unknown
Publisher	The Department of Computer Science, University of York
Volume	YCS-2003-357
Publication status	Published - 1 Jun 2003

Publication series

Name	Department of Computer Science Technical Report
Publisher	Department of Computer Science, University of York
Volume	YCS-2003-357

Cite this

@book{e70a72a0457647aa86486cead104b166,

title = "CSP/FDR2 to Handel-C translation",

abstract = "This report is adapted from a study performed for AWE in 2001 by the author while at Logica. It investigates the feasibility of using the CSP specification language and FDR2 model-checking tool, and Handel-C programming language, in combination, with FDR2 as a front-end specification and proof tool, then automatically translating the formal designs into executable Handel-C. Such an approach could provide a development path from an abstract specification to a correct executable implementation running on an FPGA.This report contains the followinga) Identification of a subset of CSP that maps closely to Handel-C. That subset is large enough to accommodate a large subset of CSP specifications. b) A sketch of a mapping from the identified CSP subset to Handel-C, suitable to be performed automatically. As proof-of-concept, the identified mappings are hand-applied to two example CSP specifications to produce Handel-C implementations.",

author = "Susan Stepney",

year = "2003",

month = jun,

day = "1",

language = "Undefined/Unknown",

volume = "YCS-2003-357",

series = "Department of Computer Science Technical Report",

publisher = "The Department of Computer Science, University of York",

}

TY - BOOK

T1 - CSP/FDR2 to Handel-C translation

AU - Stepney, Susan

PY - 2003/6/1

Y1 - 2003/6/1

N2 - This report is adapted from a study performed for AWE in 2001 by the author while at Logica. It investigates the feasibility of using the CSP specification language and FDR2 model-checking tool, and Handel-C programming language, in combination, with FDR2 as a front-end specification and proof tool, then automatically translating the formal designs into executable Handel-C. Such an approach could provide a development path from an abstract specification to a correct executable implementation running on an FPGA.This report contains the followinga) Identification of a subset of CSP that maps closely to Handel-C. That subset is large enough to accommodate a large subset of CSP specifications. b) A sketch of a mapping from the identified CSP subset to Handel-C, suitable to be performed automatically. As proof-of-concept, the identified mappings are hand-applied to two example CSP specifications to produce Handel-C implementations.

AB - This report is adapted from a study performed for AWE in 2001 by the author while at Logica. It investigates the feasibility of using the CSP specification language and FDR2 model-checking tool, and Handel-C programming language, in combination, with FDR2 as a front-end specification and proof tool, then automatically translating the formal designs into executable Handel-C. Such an approach could provide a development path from an abstract specification to a correct executable implementation running on an FPGA.This report contains the followinga) Identification of a subset of CSP that maps closely to Handel-C. That subset is large enough to accommodate a large subset of CSP specifications. b) A sketch of a mapping from the identified CSP subset to Handel-C, suitable to be performed automatically. As proof-of-concept, the identified mappings are hand-applied to two example CSP specifications to produce Handel-C implementations.

M3 - Other report

VL - YCS-2003-357

T3 - Department of Computer Science Technical Report

BT - CSP/FDR2 to Handel-C translation

PB - The Department of Computer Science, University of York

ER -