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 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. A largely separate process is then used in the implementation of such as continuous model as a digital (discrete) controller.
In the account above, the controller, whether natural or man-made, is treated first as a dynamical system and then represented computationally. We seek rather to view control as a computational phenomenon from the start, so that we can use established notions from computational logic 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.
Block diagrams are a standard engineering representation of dynamical systems, obtained from a Laplace transform. We have recently completed a pilot project, funded by Qinetiq, in which we added assertions about phase and gain of a signal to block diagrams and devised and implemented a simple Hoare logic. We were able to emulate mechanically engineers informal reasoning about phase and gain [22]. At the suggestion of Qinetiq’s control engineers we used this to prototype symbolic, automated, very general alternatives to some standard numeric tests used in engineering design [26]. This is evidence for the feasibility of our long term goal.
Thus the AIM of this project is to develop logical techniques to model continuous and discrete dynamical systems, with a focus on the needs of practical applications. Our measurable OBJECTIVES are:
(i) to establish a logical framework, assertion language and inference system for understanding and reasoning about continuous and discrete control
(ii) to validate our ideas against examples drawn from avionics and biological applications
(iii) a prototype implementation using existing methods and tools such as Simulink, Clawz and PVS.
The proposers have a strong track record in mathematics, logic and computer science. They will collaborate with Martin Hyland (Maths, Cambridge), Gordon Plotkin (Computer Science Edinburgh), Peter Saunders (Maths, Kings London), David Gilbert (Bioinformatics, Glasgow), a variety of close-at-hand mathematical experts (algebera, analysis, differential equations) in St Andrews, and industrial control engineers and computer scientists at Qinetiq (O’Halloran, Patel, Hall), SRI International (Tiwari, Rushby) and NASA Langley (Butler). In particular our earlier work benefited enormously from the patience and insight of working engineers at Qinetiq, nad we expect to continue this synergy in this project, as well as developing a new case study with Intel Research.
1 Ursula Martin, Computers, reasoning and mathematical practice, Proc 1997 NATO ASI Summer School, Springer Verlag 1999
2 A Adams, M Dunstan, H Gottliebsen, T Kelsey, U Martin and S Owre, Computer Algebra meets Automated Reasoning: Integrating Maple and PVS. in TPHOLS 2001, LNCSxxxx, Springer Verlag, 2001
3 Andrew Adams et al, VSDITLU: a verified symbolic definite integral table look-up, CADE 16, LNAI 1632, Springer 1999
4 Ursula Martin, Towards formal methods for mathematical modeling, Proc 5th NASA Formal Methods Workshop, NASA Press 2000
5 K Ogata, Modern control engineering, Prentice Hall 1997
6 E Sontag, Mathematical control theory, Springer 1998
7 MATLAB
8 R Pratt (ed), Flight control systems, IEE Press 2000
9 R Arthan, C O'Halloran et al, ClawZ: Control Laws in Z, ICFEM 2000, IEEE Press 2000
10 E Davidson, Genomic regulatory systems, Academic Press 2001
11 P Saunders, J Koeslag and J Wessels, Integral Rein Control in Physiology, J. Theor. Biol. 194 (1998) 163-173.
12 Bruce Krogh, Approximating Hybrid System Dynamics for Analysis and Control, HSCC 1999, LNCS 1569, Springer, 1999
13 M Jirstrand, Nonlinear Control System Design by Quantifier Elimination, J Symbolic Comput, 24, 137-152, 1997.
14 M Arbib and E Manes, Machines in a category, SIAM review 57 (1974), 163-192
15 M. Hasegawa, Models of Sharing Graphs, Springer 1997
16 C Gurr and K Tourlas, Towards the principled design of software engineering diagrams, in ICSE 22, pp 509-520, ACM Press 2000
17 A Edalat and A Lieutier, Domain theory and differential calculus, Proc IEEE LICS 17, IEEE Press 2002
18 A Tiwari and G Khanna, Series of abstractions for hybrid automata, in 5th HSCC 2002, LNCS 2289, Springer 2002
19 Martin Dunstan et al, Lightweight formal methods for computer algebra systems, ISSAC'98, ACM Press, 1998
20 Martin Dunstan et al, Formal Methods for Extensions to CAS, FM'99, LNCS 1709, Springer 1999
21 B Mahony, The DOVE approach to the design of complex dynamic processes, NASA/CP-2002-211736, August 2002
22 R Boulton, R Hardy and U Martin, A Hoare logic for single-input single-output continuous-time control systems, HSCC 2003, LNCS 2623 Springer 2003
23 C A R Hoare, An axiomatic basis for computer programming, Communications of the ACM, 12, 576--580 1969
24 Tobias Nipkow, Hoare Logics in Isabelle/HOL, in Proof and System-Reliability, Kluwer, 2002
25 M Gordon, Mechanizing programming logics in higher order logic, in Current trends in hardware verification and automated theorem proving, pp 387—439, Springer 1989.
26 R Hardy, Symbolic analysis of design requirements for control laws, Technical report 2002, www-theory.st-and.ac.uk/~um/HSCC
27 H Gottliebsen, Transcendental functions and continuity checking in PVS, TPHOLS 2000, LNCS 1869, Springer 2000
28 J Fleuriot, On the mechanisation of real analysis in Isabelle/HOL, TPHOLS 2000, LNCS 1869, Springer 2000
29 D Dill. A theory of timed automata. Theoretical Computer Science , 126(2):183-235,1994