Home > Archive > Functional > April 2007 > ***REMINDER:BCS-FACS/BCSWomen Joint Evening Seminar by Prof. Ursula Martin, 26 April,
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
***REMINDER:BCS-FACS/BCSWomen Joint Evening Seminar by Prof. Ursula Martin, 26 April,
|
|
| Paul.Boca@googlemail.com 2007-04-23, 8:04 am |
|
(Apologies if you receive multiple copies of this announcement)
BCS-FACS/BCSWomen Joint Evening Seminar
Design Verification for Control Engineering
Professor Ursula Martin
Queen Mary, University of London
26 April 2007
5.45pm
BCS London Offices
First Floor
The Davidson Building
5 Southampton Street
London WC2E 7HA
In the first part of this talk I'll introduce control engineering
as a new domain of application for formal methods. I'll discuss
design verification, drawing attention to the role played by
diagrammatic evaluation criteria involving numeric plots of a
design, such as Nichols and Bode plots. I'll show that symbolic
computation and computational logic can be used to discharge
these criteria and provide symbolic, automated, and very general
alternatives to these standard numeric tests, and illustrate our
work with reference to a standard reference model drawn from
military avionics.
At the heart of this work is the observation that control systems
based on linear differential equations exhibit "program-like"
phenomena such as loops and sequential composition, which allows
the development of a Hoare-style logic. While trying to understand
this phenomenon we hit upon a new abstract presentation of Hoare
Logic based on categories with feedback, which can also be used
to capture extensions of the standard Hoare logic for while
programs, e.g. the extension with pointer manipulations via
separation logic.
References:
Richard Boulton, Hanne Gottliebsen, Ruth Hardy, Tom Kelsey & Ursula
Martin,
Design Verification for Control Engineering. Integrated Formal
Methods,
4th International Conference, IFM 2004, Canterbury, UK, April 4-7,
2004,
Lecture Notes in Computer Science vol 2999, pages 21-35, Springer,
2004.
Ursula Martin, Erik Mathiesen and Paulo Oliva, Hoare Logic in the
Abstract.
Proceedings of Computer Science Logic Conference 2006. Lecture Notes
in
Computer Science vol 4207, pages 501-515, Springer, 2006.
Refreshments will be served from 5.15pm
The seminar is free of charge and open to everyone. If you would like
to
attend, please email Paul Boca [Paul.Boca@googlemail.com] your name by
24 April 2007. Pre-registration is required, as security at the BCS
Offices is tight.
|
|
|
|
|