Dependable Continuous Mathematics for Critical Systems
Professor Ursula Martin and Dr Hanne
Gottliebsen, lead this new project, in close collaboration with Qinetiq, NASA Langley, Intel Research Cambri
dge, mathematicians at Queen Mary University of London, and the Automated Reasoning G
roup in the Computer Laboratory at the University of Cambridge.
The immediate goal of the project is to develop a computational logic framework
for reasoning about dynamical systems, especially in feed-back control theory and its a
pplications, extending a pilot study concerned with Hoare logic for classical control.
It is part of a long term program to apply the techniques of computational logic to ma
thematics and its applications.
Further details about the background to the research are available at
http://www.dcs.qmu
l.ac.uk/grants/~uhmm/clcm/summary.html
You can also look at the full grant proposal for the project
http://www.dcs.qmul.ac
.uk/grants/~uhmm/clcm/prop.pdf
Project Members
Ursula Martin
Roy Dyckhoff
Hanne Gottliebsen
Henri Huijberts
Olga Lightfoot
Erik Mathiesen
Paulo Oliva
Graham White
Project Documentation
- Overview of Control System Engineering as Background for
Research into Symbolic Reasoning (PDF/PostScript)
- Slides from talk at Malvern meeting, 4 March 2002 (PDF/PostScript)
- Slides from talk at TTCP meeting in York, 9
April 2002 (PDF/PostScript)
- Avenues of Research discussion document, 18 April 2002 (PDF/PostScript)
- Slides from overview talk at St Andrews meeting, 25 June 2002
(PDF)
- Slides from talk on Proving Constraints on Nichols Plots at
St Andrews meeting, 25 June 2002 (PDF/PostScript)
- Slides from talk on Hoare Logic at St Andrews meeting, 25
June 2002 (PDF/PostScript)
- Final project report, June 2002 (PDF/PostScript)
- Symbolic Analysis of Design Requirements for Control Laws
(technical report), October 2002 (PDF/PostScript)
- Towards a Hoare Logic for
Continuous-Time Control Systems
(technical report), November 2002 (PDF/PostScript)
Publications
- A Hoare logic for single-input single-output continuous time
control systems, In Proceedings 6th International Workshop on Hybrid Systems, Computation and Control, pages 113-125,
Springer LNCS vol 2623, 2003 (PDF/PostScript)
- Design verification for control engineering, To appear in Proceedings of the Fourth International Conference on Integrated Formal Methods, LNCS xxxx, Springer 2004 (PDF)
Collaborators
Tools
Control Engineering
General
Stability
Frequency Response
Block Diagram Transformation
Researchers and Research Groups
Symbolic Reasoning
Hoare Logic
Decision Procedures
Graph Rewriting and Transformation
Researchers
Related Work
MoBIES
Hybrid Systems
Computer Algebra and Automated Reasoning
Other