BCS-FACS/BCS Women Seminar by Prof. Ursula Martin, 9 November, 5.45pm, BCS Offices, London

BCS-FACS/BCS Women Seminar by Prof. Ursula Martin, 9 November, 5.45pm, BCS Offices, London

Post by FACS FACTS » Fri, 03 Nov 2006 22:35:21


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://www.yqcomputer.com/


http://www.yqcomputer.com/



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 [ XXXX@XXXXX.COM ] your name by
BCS Offices is tight.

Location of the venue: http://www.yqcomputer.com/

FACS Evening Seminars: http://www.yqcomputer.com/

BCSWomen website: http://www.yqcomputer.com/
 
 
 

1. BCS-FACS/BCS Women Seminar by Prof. Ursula Martin, 9 November, 5.45pm, BCS Offices, London

2. *** BCS-FACS Evening Seminar by Prof. Martin Henson, 8 November 2005, 5.45pm, London ***


BCS-FACS Evening Seminar


nuZ -- a wide-spectrum logic for specification and program development


Professor Martin Henson
University of Essex


8 November 2005


5.45pm


BCS London Offices
First Floor
The Davidson Building
5 Southampton Street
London WC2E 7HA



The framework nuZ is a radical modification of the specification
language Z. The differences are as follows:

* Z is based on a partial-correctness semantics: nuZ is based on a
total-correctness semantics;

* Z identifies chaos and magic (blocking): nuZ distinguishes between
these;

* Z schema operators are not monotonic: nuZ schema operators are
monotonic;

* Z is based on equality: nuZ is based on refinement;

* Z is a specification language: nuZ is wide-spectrum;

* Z is relatively inflexible: nuZ is easily extensible;

* Z is a language: nuZ is a logic;

I will concentrate on showing how nuZ (a very tiny system) can be
extended to a full specification language; used to specify (internally)
a programming language, including action systems, and its logic; and
then used to develop programs, by refinement, from specifications.


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[ XXXX@XXXXX.COM ] by
the BCS Offices is tight.


Location of venue:

http://www.yqcomputer.com/

3. REMINDER: BCS-FACS Evening Seminar by Prof. Martin Henson, 8 November 2005, 5.45pm, London, UK

4. *** BCS-FACS Evening Seminar by Prof. Martin Henson, 8 November 2005, 5.45pm, London ***

5. BCS-FACS Evening Seminar by Prof Mark Harman: Testability transformation, 26 May, BCS London Offices, UK

6. *** BCS-FACS Evening Seminar by Prof. Steve Schneider, 3 March 2008, BCS London Offices, UK

7. *** BCS-FACS Seminar by Prof. Michael Jackson, 7 February 2007, 5.45pm, London

8. *** BCS-FACS Evening Seminar by Prof. Michael Butler, 10 May 2007, 5.45pm, London,UK ***

9. *** BCS-FACS Seminar by Prof. Michael Jackson, 7 February 2007, 5.45pm, London

10. *** BCS-FACS Evening Seminar by Prof. Michael Butler, 10 May 2007, 5.45pm, London,UK ***

11. BCS-FACS Evening Seminar by Mark Harman, Testability Transformation, 26 May, BCS London Offices, UK

12. BCS-FACS/FME Evening Seminar by Cliff Jones, 24 April 2006, 5.45 pm, London