[Prev][Next][Index][Thread]
Formal Methods Day at Royal Holloway
ROYAL HOLLOWAY, UNIVERSITY OF LONDON
DEPARTMENT OF COMPUTER SCIENCE
FORMAL METHODS DAY - Thursday 27 November 1997
1997/98 is the 30th anniversary year of the Department of Computer
Science at Royal Holloway, University of London. As part of the
anniversary celebrations, there will be a series of one-day colloquia
organised by the research groups in the department.
The first of these colloquia is the Formal Methods Day, to be held at
Royal Holloway on Thursday 27th November 1997. The programme will
consist of three invited lectures, which between them will cover a
range of formal methods topics, from theory to industrial
practice. The speakers and their titles are as follows (abstracts are
attached below).
Professor Samson Abramsky, Department of Computer Science,
University of Edinburgh:
Completing Strachey's Programme:
towards a mathematical theory of realistic programming languages
Dr Bent Thomsen, ICL, Research & Advanced Technology, Group Technical
Directorate:
Mobile Agents, Facile and Theory of Computing
Dr Gerard J Holzmann, Computing Principles Research Dept,
Bell Labs, Murray Hill, NJ, USA:
Proving properties of concurrent systems:
The theory and practice of a model checker
The programme includes lunch in the famous Picture Gallery at Royal
Holloway. All are welcome to attend. There is no charge for the day,
but advance booking is essential. Travel information and maps will be
available after booking. To reserve your place, contact
Janet Hales, Departmental Events Co-ordinator,
Department of Computer Science,
Royal Holloway, University of London,
Egham,
Surrey
TW20 0EX
Tel: 01784 443432
Fax: 01784 439786
Email: J.Hales@dcs.rhbnc.ac.uk
Further information is also available from
http://www.dcs.rhbnc.ac.uk/events/fmgday.shtml
PROGRAMME
10.30 am Coffee
11.00 am Welcome and Introduction, followed by
Lecture 1: Professor Samson Abramsky
12.00 pm Questions and Discussion
12.30 pm Lunch
2.00 pm Lecture 2: Dr Bent Thomsen
3.00 pm Questions and Discussion
3.15 pm Tea
3.45 pm Lecture 3: Dr Gerard Holzmann
4.45 pm Questions and Discussion
5.00 pm Close
ABSTRACTS
Prof Samson Abramsky, Department of Computer Science,
University of Edinburgh:
Completing Strachey's Programme:
towards a mathematical theory of realistic programming languages
In his pioneering work on denotational semantics, summarized in his
1976 monograph with Robert Milne, "A Theory of Programming Language
Semantics", Christopher Strachey mapped out a programme of giving a
precise mathematical account of the semantics of a wide-spectrum
modern programming language, as a basis for a rigorous approach to
software engineering. One formulation of this in current terms is: to
give a fully abstract semantics for languages such as Standard ML.
The underlying aim is to give a definitive analysis of concepts such
as procedures, references and local state, continuations and
exceptions, which are at the core of today's programming languages,
including object-oriented languages such as Java. This version of
Strachey's programme has seemed well out of reach for the 20 years
following the publication of his monograph. Capturing the semantics
even of the functional fragment in a precise way eluded many attempts;
and dealing properly with non-functional features such as local state
seemed to present significant additional problems. However, the
situation has changed following recent progress in a novel approach to
semantics based on modelling computation as a game, in which a system
interacts with its environment like a player pitting his wits against
an adversary. There is now a real prospect of completing (this version
of) Strachey's programme. The key ideas of games semantics will be
presented informally, and the progress towards completing Strachey's
programme, and some key issues for future research, will be discussed.
Dr Bent Thomsen, ICL, Research & Advanced Technology, Group Technical
Directorate:
Mobile Agents, Facile and Theory of Computing
Mobile agents, i.e. pieces of programs that can be sent around
networks of computers, are starting to appear on the Internet. Such
programs may be seen as an enrichment of traditional distributed
computing. Since mobile agents may carry communication links with
them as they move across the network, they create very dynamic
interconnection structures that can be extremely complex to analyse.
In this talk we give a short introduction to mobile agents, discuss
their potential and describe a proof-of-concept implementation called
Mobile Service Agents.
Mobile Service Agents are written in the Facile language. Facile's
basis on formal process models for mobility (e.g., the pi-calculus and
CHOCS) and on functional programming languages makes the language well
suited for developing a significant class of mobile applications.
We discuss how advanced semantic concepts such as advanced type
systems, true concurrency, causality and locality can be used to
analyse Mobile Agent based systems.
Finally we discuss challenges that Mobile Agents bring to Theory of
Computing.
Dr Gerard J Holzmann, Computing Principles Research Dept, Bell Labs, Murray
Hill, NJ, USA:
Proving properties of concurrent systems:
The theory and practice of a model checker
The development of any non-trivial piece of software is an
intellectually challenging task. This much has been known for as long
as computers have existed. The question still is what we can do about
this. In the sixties and seventies our attempt was to develop a new
discipline of programming, and new proof techniques that would allow
us to attain reliable software by construction. But the complexity of
computer systems increases much more rapidly then our ability to
understand and control them. And also today, buggy software is still
very much a fact of life. In this talk I'll describe a different
attempt to confront this crisis. We consider the construction of a
piece of software as just another engineering task. The task is most
constructively handled by a technique that is borrowed from other
engineering disciplines: by prototyping and model building. A model
is an abstraction of a planned system that has the advantage that it
can be analyzed thoroughly for its intended and unintended design
characteristics. Considerable practical experience with this style of
model checking for hardware and software components has been gained in
the last few years. I'll discuss the theoretical basis for an
efficient on-the-fly model checking system that supports this style of
software design, and will discuss some recent applications.