Control Law Diagrams in Circus

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.

• Type: Conference
• Year: 2005
• Where: FM
• Authors: Ana Cavalcanti, Phil Clayton, Colin O'Halloran
• Keywords: Block Diagrams, Discrete-time Block Diagrams, FM 2005, Refinement Calculus