The Industrial Use of Formal Methods: Experiences of an Optimist

Jonathan BowenDate/Time:
Thursday 10 January 2013, 6.00pm - 8.00pm

The Davidson Building, 5 Southampton Street, London WC2E 7HA. The nearest underground stations are Covent Garden and Charing Cross.

Prof Jonathan Bowen


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.

Note: This will be a joint meeting with the FACS (Formal Aspects of Computing Science) group. The talk is suitable for a general audience with an interest in software engineering.

About the Speaker:

Prof. Jonathan P. Bowen, FBCS, FRSA, is Chair of Museophile Limited, an IT consultancy company. He has also been an Emeritus Professor at London South Bank University since 2007. In May 2012, he was a visiting academic at the Pratt Institute in New York. He has also been a Visiting Professor at the University of Waikato in New Zealand and the University of Westminster. 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 on computing and museum-related topics, among other areas. Bowen is a Fellow of the British Computer Society and of the Royal Society of Arts. He is a Liveryman of the Worshipful Company of Information Technologists in London. He has an MA degree in Engineering Science from Oxford University.

BCS Formal Aspects of Computing Science Specialist Group (FACS) website


Free. To gain admission please email your name to our Membership Secretary, Algirdas Pakstas, at in advance of the meeting. Attendance lists will normally be finalised on the Monday preceding each meeting but late admission may be accepted by signing in to the Davison Building as a visitor.


View the slides for this event (PDF)
View the YouTube video of the event