[Apologies if you receive multiple copies of this announcement]
BCS-FACS Evening Seminar Series -- Joint Event with BCSWomen Specialist
Group
Design verification for control engineering
Professor Ursula Martin
Queen Mary University of London
9 November 2006
5.45pm start
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." in Integrated
Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK,
April 4-7, 2004, Lecture Notes in Computer Science vol 2999, pp. 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, 2006, pages 501-515, Springer 2006
http://springerlink.metapress.com/content/gxj1n2gtq11cly8h/?p=48763561ce3542caac39908fe87202c9&pi=1
http://www.springerlink.com/content/68245wk122px6537/
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 [[log in to unmask]] your name by 6 Nov 2006.
Pre-registration is required,
as security at the BCS Offices is tight.
Location of the venue: http://www.bcs.org/upload/img/londonsscolour.jpg
FACS Evening Seminars: http://www.bcs-facs.org/events/EveningSeminars
BCSWomen website: http://www.bcs.org.uk/bcswomen/
