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 these diagrams, and can cover a wider range of blocks. Moreover, the Circus refinement calculus can be used to verify implementations, and reason about the block diagrams. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Cavalcanti, A., Clayton, P., & O’Halloran, C. (2005). Control law diagrams in Circus. In Lecture Notes in Computer Science (Vol. 3582, pp. 253–268). Springer Verlag. https://doi.org/10.1007/11526841_18
Mendeley helps you to discover research relevant for your work.