The Industrial Use of Formal Methods: Experiences of an Optimist

Speaker:	Prof. Jonathan P. BOWEN
		London South Bank University /
		University of Westminster / Museophile Limited
		United Kingdom

Title:		"The Industrial Use of Formal Methods: Experiences of an
		 Optimist"

Date:		Monday, 25 October 2010

Time:		4:00pm - 5:00pm

Venue:		Lecture Theater F (near lifts 25/26), HKUST

Abstract:

Formal methods aim to apply mathematically-based techniques to the
development of computer-based systems, especially at the specification
level, but also down to the implementation level. This aids early
detection and avoidance of errors through increased understanding. It is
also beneficial for more rigorous testing coverage. This talk presents the
use of formal methods on a real project. The Z notation has been used to
specify a large-scale high integrity system to aid in air traffic control.
The system has been implemented directly from the Z specification using
SPARK Ada, an annotated subset of the Ada programming language that
includes assertions and tool support for proofs. The Z specification has
been used to direct the testing of the software through additional test
design documents using tables and fragments of Z. In addition, Mathematica
has been used as a test oracle for algorithmic aspects of the system. In
summary, formal methods can be used successfully in all phases of the
lifecycle for a large software project with suitably trained engineers,
despite limited tool support

*******************
Biography:

Prof. Jonathan P. Bowen, FBCS, FRSA, is Chair of Museophile Limited, an IT
consultancy company. He is also a Visiting Professor at University of
Westminster since 2010 and an Emeritus Professor at London South Bank
University since 2007. From 2007-2009, he was a Visiting Professor at the
King's College London. In 2007, he was a visiting academic at University
College London; in 2008, he was a visiting lecturer at Brunel University
and during 2008-2009 he worked on a large industrial high integrity
software engineering project using formal methods. Previously he was at
the University of Reading, the Oxford University Computing Laboratory and
Imperial College, London. He has been involved with the field of computing
in both industry and academia since 1977, specializing in software
engineering in general and formal methods in particular. In 2002, Bowen
founded Museophile Limited with the original aim to help museums online.
He is an enthusiastic contributor to Wikipedia in the area of museums and
on computing topics. Bowen is a Fellow of the British Computer Society and
of the Royal Society of Arts. He holds the Freedom of the Worshipful
Company of Information Technologists and is a member of the ACM and IEEE.
He has an MA degree in Engineering Science from Oxford University.