%T A Step Towards Refining and Translating B Control Annotations to Handel\-C
%A  Wilson Ifill,  Steve Schneider
%E  Alistair A. McEwan,  Steve Schneider,  Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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&\[sh]8217; 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&\[sh]8217;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.