Department of Computer Science

Control Law Diagrams

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

  1. a semantics for discrete-time control diagrams to capture both their functionality and inherent concurrency;
  2. a refinement technique to support development and verification of implementations of diagrams;
  3. refinement strategies and laws tailored for the diagrams models and implementations;
  4. automated support for the application of the refinement techniques.

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.


(Top of the page)

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599