Published in

Wiley, Concurrency and Computation: Practice and Experience, 8(22), p. 1023-1048, 2010

DOI: 10.1002/cpe.1427

Links

Tools

Export citation

Search in Google Scholar

A step towards refining and translating B control annotations to Handel-C

Journal article published in 2010 by Wilson Ifill, Steve A. Schneider
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Orange circle
Postprint: archiving restricted
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO

Abstract

Research augmenting B machines presented at B2007 has demonstrated how fragments of control flow expressed as annotations can be added to associated machine operations, and shown to be consistent. This enables designers' understand- ing about local relationships between successive operations to be captured at the point the operations are written, and used later when the controller is developed. This paper introduces several new annotations and I/O into the framework to take advantage of hardware's parallelism and to facilitate refinement and tra nslation. To support the new annotations additional CSP control operations are added to the control language that now includes: recursion, prefixing, external choice, if-th en-else, and sequencing. We informally sketch out a translation to Handel-C for prototyping.