| BRITISH COMPUTER SOCIETY FACS SPECIALIST GROUP |
|
|
Formal Aspects of Computing Science
BCS-FACS Evening Seminar Series
Joint Event with BCS Women
Postponed due to illness
|
|
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 your name by 8 November 2006. Pre-registration is required, as security at the BCS Offices is tight. |
| Formal Aspects of Computing Science |
|
Copyright © BCS-FACS |
