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.