Paper Details

A Step Towards Refining and Translating B Control Annotations to Handel-C

Authors: Ifill, Wilson, Schneider, Steve

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’ understanding 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 translation. To support the new annotations additional CSP control operations are added to the control language that now includes: recursion, prefixing, external choice, if-then-else, and sequencing. We informally sketch out a translation to Handel-C for prototyping.

Proceedings:

Communicating Process Architectures 2007, Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch, 2007, pp 399 - 424 published by IOS Press, Amsterdam

Files: PDF

This record in other formats:

Web page: BibTEX, Refer
Plain text: BibTEX, Refer

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.