Anthony Hall

FME invited talk: Correctness by construction: Integrating formality into a commercial development process
Tuesday July 23rd 09:00-10:00 in auditorium 2

Abstract

This paper describes a successful project where we used formal methods as an integral part of the development process for a system intended to meet ITSEC E6 requirements. The system runs on commercially available hardware and uses common COTS software. We found that using formal methods in this way gave benefits in accuracy and testability of the software, reduced the number of errors in the delivered product and was a cost-effective way of developing high integrity software. Our experience contradicts the belief that formal methods are impractical, or that they should be treated as an overhead activity, outside the main stream of development. The paper explains how formal methods were used and what their benefits were. It shows how formality was integrated into the process. It discusses the use of different formal techniques appropriate for different aspects of the design and the integration of formal with non-formal methods.

About Anthony Hall

Anthony Hall is a Principal Consultant with Praxis Critical Systems Ltd. He is a specialist in requirements and specification methods and the development of software-intensive systems.

Anthony has worked for many years on the development of critical operational systems. During this time he has pioneered the application of formal methods to industrial practice. He was for example chief designer on CDIS, a successful air traffic information system and on a Certification Authority developed to ITSEC E6 standards.

Anthony has carried out requirements engineering for many projects in areas including aviation, railway signalling, secure systems and communications. He has also been closely involved in academic and professional developments in requirements engineering. Together with colleagues in Praxis Critical Systems he has brought together extensive practical experience and the latest research findings to develop REVEAL, a principled yet practical approach to requirements engineering.

As well as carrying out projects and consulting for clients, Anthony teaches and lectures widely. He has been a keynote speaker at the International Conference on Software Engineering, at the IEEE conference on Requirements Engineering and other conferences. He has published several papers on formal methods. Anthony received an MA and a D.Phil. from Oxford. He is a Fellow of the British Computer Society and a Chartered Engineer.

Selected publications:

  1. Correctness by Construction: Developing a Commercial Secure System, Anthony Hall and Roderick Chapman, IEEE Software Jan/Feb 2002, pp 18-25. Available from http://www.sparkada.com.
  2. Taking Z Seriously, in ZUM '97: The Z Formal Specification Notation, Springer (1997).
  3. What is the Formal Methods Debate About?, IEEE Computer, April 1996, pp 22-23.
  4. Using Formal Methods to Develop an ATC Information System, IEEE Software, March 1996, pp 66-76. Reprinted in Industrial-Strength Formal Methods in Practice, M.G. Hinchey &apm; J.P. Bowen, Springer (1999)
  5. Specifying and Interpreting Class Hierarchies in Z, in Z User Workshop, Cambridge 1994, ed. J. P. Bowen and J. A. Hall, Springer (1994)
  6. Integrating Methods in Practice, in Formal Methods in Systems Engineering, ed. P. Ryan and C. Sennett, Springer-Verlag (1993)
  7. Seven Myths of Formal Methods, IEEE Software, September 1990, pp 11-19.
  8. Using Z as a Specification Calculus for Object-oriented Systems, pp 290-318 in Proceedings of VDM90, Lecture Notes in Computer Science no 428.