Atomicity failure and the retrenchment atomicity pattern, Richard Banach, Czesław Jeske, Anthony Hall and Susan Stepney, Formal Aspects of Computing, DOI: 10.1007/s00165-011-0216-1, 2011
Non-ACID timing aspects of a simple Air Traffic Control system are described and specified as a retrenchment problem, and the treatment is generalised to yield the Retrenchment Atomicity Pattern. The utility of the pattern is confirmed against a number of different case studies.
Integrating Z Into Large Projects: Tools and Techniques, Anthony Hall, in Short Papers of the ABZ 2008 Conference, ed. Egon Börger, Michael Butler, Jonathan Bowen and Paul Boca. 
This paper describes an approach to writing Z specifications that integrates the mathematics with natural language and domain specific notations so that the specifications are accessible to all stakeholders. It describes the Z Word Tools that I have developed to support this process using the most readily acceptable document preparation tool, Microsoft Word.
Software Verification and Software Engineering: a Practitioner’s Perspective, Anthony Hall, in Verified Software: Theories, Tools, Experiments, ed Bertrand Meyer and Jim Woodcock, LNCS 4171, Springer, pp70 – 73, 2005.
A critique of the “Grand Challenge” to produce a verifying compiler. The published version contains a transcript of some discussion as well as the abstract available from the PDF link.
Realising the Benefits of Formal Methods, Anthony Hall, Formal Methods and Software Engineering, LNCS 3785, Springer, pp1 – 4, 2005. A longer version of this paper is available in Computer Society of India Communications, Vol. 31, Issue 2, May 2007. ISSN: 0970-647X.
What are the real benefits of formal methods and Why should we care about them? When and Where should we expect to use hem, and Who should be involved? I suggest some answers to those questions and describe one approach, Correctness by Construction, that has achieved practical success on several real industrial developments. Based on this I propose some challenges for formal methods research.
Z Styles for Security Properties and Modern User Interfaces,Anthony Hall, Formal Aspects of Security, LNCS 2629, Springer, pp152 – 166, 2002.
This is a technical paper about how to use Z to define security requirements and to capture the important behaviour of a system with a WIMP style user interface.
Correctness by Construction: Integrating Formality into a Commercial Development Process, Anthony Hall, Proceedings of International Symposium of Formal Methods Europe, LNCS 2391, Springer, pp224 – 233, 2002.
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.
Correctness by Construction: Developing a Commercial Secure System, Anthony Hall and Roderick Chapman, IEEE Software Jan/Feb 2002, pp18-25.
Praxis Critical Systems Ltd developed a secure certification authority (CA) for smart cards. The CA had to satisfy demanding performance and usability requirements while meeting stringent security constraints. We used a systematic process from requirements elicitation through formal specification, user interface prototyping, rigorous design and coding in SPARK, a secure Ada subset, to ensure that these objectives were achieved. System validation included tool-assisted checking of a formal process design, top down testing system testing with coverage analysis and static analysis of the code. The system uses COTS hardware and software but no reliance is placed on correctness of COTS for critical security properties. We show how a process which achieves normal commercial productivity can deliver a system which is proving highly reliable in daily use, meeting all its throughput and usability goals.
What does Industry Need from Formal Specification Techniques?, Anthony Hall, in Proceedings of 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques, October 1998, pp 2-7.
In this paper I examine what role formal techniques play in practical development. I examine the different ways that formality can be used and where it is and is not effective. I discuss what we can already do well and where more research is needed to support industrial practice.
Do Interactive Systems Need Specifications?, Anthony Hall, in Design, Specification and Verification of Interactive Systems, Springer, 1997.
This paper argues that abstract specifications complement prototypes and that both techniques have a role to play in developing systems.
Taking Z Seriously, Anthony Hall, in ZUM ’97: The Z Formal Specification Notation, Springer 1997.
A discussion of the strengths and weaknesses of Z and where it is appropriate to use it as a practical specification language.
What is the Formal Methods Debate About?, IEEE Computer, April 1996, pp 22-23. (Available via the Digital Library)
A position statement contributed to a special issue on formal methods.
Using Formal Methods to Develop an ATC Information System,Anthony Hall, IEEE Software, March 1996, pp 66-76. (Available via the Digital Library)
Reprinted in Industrial-Strength Formal Methods in Practice, M.G. Hinchey & J.P. Bowen, Springer, 1999.
CDIS is a distributed real-time information system supporting air traffic controllers. It was developed using advanced software engineering techniques including the extensive use of formal methods for specification and design. This article describes how formal methods were used. It shows that they can improve quality at no extra cost and that they are applicable to a large, demanding project.
Integrating Methods in Practice, Anthony Hall, in Formal Methods in Systems Engineering, ed. P. Ryan and C. Sennett, Springer-Verlag, 1993.
Seven Myths of Formal Methods, Anthony Hall, IEEE Software, September 1990, pp 11-19. (Available via the Digital Library)
Reprinted in Software Engineering: A European Perspective, ed. R.H.Thayer & A.D. McGettrick, IEEE Computer Society Press (1992) and High Integrity System Specification and Design, J.P. Bowen & M.G. Hinchey, Springer, 1999.
Seven widely held conceptions about formal methods are challenged. These beliefs are variants of the following: formal methods can guarantee that software is perfect; they work by proving that the programs are correct; only highly critical systems benefit from their use; they involve complex mathematics; they increase the cost of development; they are incomprehensible to clients; and nobody uses them for real projects. The arguments are based on the author’s experiences. They address the bounds of formal methods, identify the central role of specifications in the development process, and cover education and training.
This won the Best Paper award and has been widely cited.
Specifying and Interpreting Class Hierarchies in Z, Anthony Hall, in Z User Workshop, Cambridge 1994, ed. J. P. Bowen and J. A. Hall, Springer, 1994.
This paper gives formal meaning to the ideas of class and subclassing in object-oriented systems and explains how to specify class properties in Z.
Using Z as a Specification Calculus for Object-oriented Systems,Anthony Hall, in Proceedings of VDM90, Lecture Notes in Computer Science no 428, pp 290-318.
This explains how to structure a Z specification in an object-oriented style, allowing one to specify the properties of individual objects and calculate the properties of the system as a whole.