Design Verification for Control Engineering
Richard J. Boulton, Hanne Gottliebsen1, Ruth Hardy2, Tom Kelsey2, and
Ursula Martin1
1 Queen Mary University of London,
Ursula.Martin@dcs.qmul.ac.uk
2 University of St Andrews
Abstract. We introduce control engineering as a new domain of ap-
plication for formal methods. We discuss design verification, drawing
attention to the role played by diagrammatic evaluation criteria involv-
ing numeric plots of a design, such as Nichols and Bode plots. We show
that symbolic computation and computational logic can be used to dis-
charge these criteria and provide symbolic, automated, and very general
alternatives to these standard numeric tests. We illustrate our work with
reference to a standard reference model drawn from military avionics.
1 Introduction
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 want to solve the dual problem of constructing
a system with certain properties. Traditionally, control is treated as a mathe-
matical 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. A largely separate process is then
used in the implementation of such as continuous model as a digital (discrete)
controller.
Block diagrams are a standard engineering representation of dynamical sys-
tems, obtained from a Laplace transform. In a recent paper [3] we added as-
sertions about phase and gain of a signal to block diagrams and devised and
implemented a simple Hoare logic. We were able to emulate mechanically engi-
neers informal reasoning about phase and gain. We also prototyped symbolic,
automated, very general alternatives to some standard numeric tests used in
engineering design, and it is this work which forms the main result of this paper.
We replace numeric plots with symbol manipulation in the computer algebra sys-
tem Maple and the theorem prover PVS. This in turn exploited our Maple-PVS
system [12], and GottliebsenO˜s PVS continuity checker [13].
Control engineering is a large subject: we intend to focus on those aspects
which are to a control engineer fairly standard and widely used in practice [25].
E. Boiten, J. Derrick, G. Smith (Eds.): IFM 2004, LNCS 2999, pp. 21–35, 2004.
c
© Springer-Verlag Berlin Heidelberg 2004

22 R.J. Boulton et al.
Optimal control assumes that a model of the system is available and one wants to
optimise its behaviour, using the calculus of variations and so forth: for example
pre-computing a desired flight-path for a spacecraft. Feedback control compen-
sates for uncertainty in the model by using feedback to correct for deviations for
desired behaviour: for example if the spacecraft strays off course. Models vary
according to the application: for example differential equations are used when
modelling a continuous signal, but these are replaced by difference equations
when modelling a sampled signal as used in digital systems. In reasoning about
such systems we are interested not only in the solutions, but in their properties.
These include the time response, stability, frequency response and behaviour
under perturbation. The time response considers features such as the time taken
for a property of the system (e.g. the cruising speed of a car) to reach the desired
value, and by how far it overshoots before settling at the desired value. Stability
analysis considers whether the system will always settle into a steady state fol-
lowing a change to the input(s). An output of an unstable system may increase
out of control or oscillate. Frequency response considers the amplitude and phase
shift of the output signal when the system is presented with a sinusoidal input.
The analysis considers input signals with a range of frequencies.
In practice systems are rarely linear: non-linear systems are generally treated
O`locallyO´ by linearising at points of interest, but O`globalO´ behaviour is sub-
ject of much research and raises subtle questions in differential and algebraic
geometry.
In O`classicalO´ control a Laplace transform is applied to a linear system
to obtain a representation as a transfer function, a rational function over the
complexes. Analysis of properties, such as frequency and response of the control
system, is in terms of the position of its roots and poles in the complex plane. So
called O`modernO´ control considers a state-space representation, which replaces
a single differential equation with a system of simultaneous equations in the state
variables, and analyses the system via properties of the eigenvalues of a related
matrix. Both frameworks can be extended from SISO (single input) to MIMO
(multiple input) systems.
Block diagrams are often used to represent systems with feedback graphi-
cally, for example in classical control a block diagram is a directed graph whose
edges are labelled by rational functions over the complexes. They also allow more
general representation of components described only by their input/output be-
haviour.
Software such as the widely used Mathworks Simulink [21], the industry
standard in avionics and automotive applications, supports numerical tests and
simulations. A number of standard tests are used for prediction and analysis:
for example the Nichols plot is a numerical test which investigates stability. It
displays the steady state behaviour of a O`classicalO´ control system in terms of
the phase and gain of a sinusoidal input. We shall see below how some of the
control requirements of fighter aircraft are specified in terms of acceptable paths
in this plot [26].
In practice man-made control systems are typically digital embedded soft-
ware systems, which use sampled, rather than continuous time. These can be