Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory
Abstracts
Computer Laboratory > Abstracts

Seminars will be held in the Lecture Theatre 1 - William Gates Building, Computer Laboratory at 4.15pm
   
See also:

 Networks & OS seminars
 Security seminars
 Logic and Semantics seminars
 Additional meetings
 weekly timetable
for other seminars

Reasoning about Digital Control

Ursula Martin **

Queen Mary University of London and University of Cambridge

To control an object means to influence its behaviour so as to achieve a desired goal. Control systems may be natural mechanisms, such as cellular regulation of genes and proteins by the gene control circuitry in DNA. They may be man-made - an early mechanical example was Watt's steam governor - but today most man-made control systems are digital, for example fighter aircraft or CD drives. In genomics we want to identify the control mechanism from observations of its properties: in engineering we face the dual problem of building a system which has certain properties.

Traditionally, control is treated as a mathematical phenomenon, modelled by continuous or discrete dynamical systems. Numerical computation is used to test and simulate these models, for example MATLAB is an industry standard in avionics. We seek rather to view control as a computational phenomenon from the start, so that we can use established logical notions to understand and reason about it. This is a familiar idea in other fields: for example the representation of hardware devices as state-machines allows the use of model-checking to reason about temporal aspects.

So far we have completed a pilot project, funded by Qinetiq, in which we viewed standard engineering block diagrams as a specification, extended them with assertions about phase and gain of a signal, implemented a simple Hoare logic, and showed that it formalised engineers informal reasoning. We used this idea to prototype symbolic, automated, very general alternatives to some standard numeric tests.

This is joint work with Richard Boulton and Ruth Hardy.

**Ursula Martin is Professor of Computer Science and Director of Research in Computer Science at Queen Mary University of London, where she is a member of the Logic and Foundations research group. She is currently seconded part-time to the Computer Laboratory as Director of the Women@CL project.

Wednesday Seminars

Click here for previous seminars.