The Industrial Use of Formal Methods: Experiences of an Optimist

by Professor Jonathan P. Bowen, London South Bank University / University of Westminster

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.

Keywords:
Software engineering; high integrity systems; air traffic control; software testing; formal methods; Z notation

Note: The talk is suitable for a general audience with an interest in software engineering.

Short 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 is a Liveryman in the Worshipful Company of Information Technologists and a member of the ACM and IEEE. He holds an MA degree in Engineering Science from Oxford University.