|
| EPSRC Reference: |
GR/S31242/01 |
| Title: |
Logic structures for control |
| Principal Investigator: |
Professor UHM Martin |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Computer Science |
| Organisation: |
Queen Mary, University of London |
| Scheme: |
Standard Research |
| Starts: |
01 March 2004 |
Ends: |
31 March 2007 |
Value (£): |
232,877
|
| EPSRC Research Topic Classifications: |
| Control Systems Engineering, Integration and Autonomy |
Fundamentals of Computing |
| Logic and Combinatorics |
Numerical Analysis |
|
| EPSRC Industrial Sector Classifications: |
| Aerospace, Defence and Marine |
Information Technologies |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
|
This proposal concerns the interpretation of the mathematics of feedback control as a computational phenomenon. It is part of a long term program to apply the techniques of computational logic to mathematics and its applications. We will extend work done on a pilot project for Qinetiq, in developing a Hoare logic for a fragment of classical control, represented by block diagrams, to a larger class of control systems, including state space and MIMO models. We will develop a semantics and assertion language for these, and develop case studies in avionics and biology.
|
| Final Report Summary |
|
What do flight control systems and computer programmes have in common? Both can be structured in terms of simple primitives combined using notions of sum, product and feedback or looping. Hoare logic is a well-established way of doing logical reasoning about programmes so you can predict their behaviour without running them. This project invented a Hoare logic for control systems. It did it using a branch of mathematics called category theory - we devised a more general structure and a process for autmatically creating hoare logics form it, and them showed that our method applied to control systems and stanard Hoare logic. We also built some software, the NRV system, whcih applied our techniques to autmatically check Nicholls plots, which are a technique used in validating designs of control systems.
|
| Further Information: |
|
| Organisation Website: |
http://www.qmul.ac.uk |
|
|