Control law diagrams are routinely used by engineers in the design of control systems. Yet, the analysis of their implementations is achallenge. We propose to provide
We plan to use Circus and to reuse existing industrial tools that produce partial models of discrete-time block diagrams using Z and CSP independently. By using a combined language, we can cover a more comprehensive diagrammatic notation. Moreover, the Circus refinement theory is a sound basis for the definition of reasoning and development techniques. We propose to carry out the scientific ground work for building a tool that produces complete models of diagrams, and supports certification of their implementations.
What we propose is a novel application of refinement techniques of program development: implementation of control law diagrams. By giving Circus model to control law diagrams, we provide a strategy to generate Circus specifications for the implementations. The structure of the specifications will follow regular patterns, which we can exploit: specialised refinement rules can be used to develop implementations and reason about diagrams. Their specialised nature favours a much higher degree of automation than that achieved using general techniques. Much of the formality is made invisible. More detailed information refers to publications and tools.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599