Abstract. Control diagrams are routinely used by engineers in the design of control systems. Yet, currently the formal verification of programs that implement the diagrams is a challenge. We present a strategy to translate block diagrams to Circus, a notation that combines Z, CSP, and a refinement calculus. This work is based on existing tools that produce Z and CSP specifications from discrete-time block diagrams. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of the diagrams, and can cover a wider range of blocks. Moreover, the Circus refinement calculus can be used to derive or verify implementations, and reason about the block diagrams.