The term "formal methods" covers the use of mathematically precise notations to specify and reason about systems. This paper is mainly concerned with formal methods for software and emphasises deployments that have taken place in the UK. 1 As well as mentioning some of the important scientific contributions, emphasis is placed on the application and deployment of technical ideas and their tool support.
Both of the authors of this paper believe that the use of formal methods is essential for the creation of high-quality software. This paper is, however, not a sales pitch for such methods. What it sets out to do is to review some actual deployments, to be frank about drawbacks as well as report successes and to identify factors that have either aided or impeded the deployments.
There is no claim that this paper reports on all (nor even the most important) applications of formal methods; [WLBF09] offers a broader survey. Given that 1 Companion papers in this edition of Annals cover other European countries. a selection had to be made, it felt reasonable to choose applications where the authors had personal knowledge or at least had direct access to colleagues with such knowledge.
There is no attempt here to claim that formal approaches are a panacea in the sense that they would solve all of the problems in the software industry. For example, the question of how to argue that a (formal or informal) specification actually meets the needs of users is a huge challenge -the wise writings of Michael Jackson such as [Jac00] are a good starting point here. Furthermore, there is the challenge of designing systems that are dependable when used in conjunction with faulty components (including hardware and human) -in this area [BGJ06, RT13] are useful starting points. Tony Hoare's paper on the axiomatic basis of programming languages [Hoa69] is the foundation stone of a significant portion of the work on formal methods. 2 In tandem with notations that have been used to provide abstract models of complex systems (e.g. VDM [Jon80] , Z [Hay93] , B [Abr96] and Event-B [Abr10a]) Hoare's ideas permeate many of the applications in the body of this paper. Robin Milner's LCF [GMW79] system provided a model for many of the theorem proving assistants that have been developed. 3 UK computer scientists have also made major contributions to concurrency research (e.g. Milner's CCS [Mil80] and Hoare's CSP [Hoa85] ).
One technical area where UK researchers have made crucial contributions is in the semantics of programming languages; although this plays a small part in the rest of the paper, Section 2 outlines this research and identifies some of its applications. We decided against trying to follow a strict timeline for the remaining sections. This is partly because the various strands of the story overlap heavily in time but we also felt that the lessons could be more clearly illustrated by looking at different modes of engagement. Beyond Section 2, the structure of the paper is that Section 3 considers initiating academic/industry collaboration using consultants, Section 4 reports on some projects where the expertise was in-house, Section 5 identifies some factors that have an impact on any deployment; conclusions are summarised in Section 6.
Although the bulk of this paper is concerned with the development of programs, there are two reasons to address research on programming languages: this was one of the first areas where is was realised that formalism could make a contribution and the UK played a significant part in the development of such research.
The study of languages is sometimes referred to as "semiotics". 4 For programming languages, most interest is in their syntax (covering content and structure) and semantics (or meaning). Finding suitable notations to define the syntax, or content, of programming languages was settled both early and broadly uncontroversially. The ALGOL 60 language was described in [BBG + 60] using Backus Normal Form 5 (often referred to as Backus Naur Form). 6 Variants of BNF have been developed including Extended BNF [Wir77] and, also from Niklaus Wirth, a graphical representation referred to as Railroad Diagrams. All of these notations perform essentially the same function and there is little doubt as to their usefulness. One bonus from using such formal descriptions of the syntax of programming languages is that they can be employed to generate parsers for the front-ends of language translators. This does bring some additional concerns about ambiguity and efficiency but, again, there is broad consensus on how to resolve these more detailed points.
The problems of finding ways to describe the semantics or meaning of programming languages has proved far more challenging. A landmark conference was held in Baden-bei-Wien in 1964. This, first ever, IFIP working conference focussed on the subject of Formal Language Description Languages and most of the talks addressed proposals for ways to describe formally the semantics of programming languages. One paper that had considerable influence on the work of the IBM Laboratory in Vienna was by the American John Mc-Carthy. In [McC66] , 7 he constructed an abstract interpreter for Micro-Algol. (Essentially, an interpreter takes a program and a starting state and iteratively computes its final state; McCarthy used the adjective "abstract" to indicate that the metalanguage in which the interpreter was written was limited and mathematically tractable.) This technique provided an operational semantics for a very small language.
The influence of work at the IBM Vienna Lab on UK research becomes important below. The phase in the 1960s saw the ideas of operational semantics extended and applied to the huge PL/I programming language. Their techniques became known as the Vienna Definition Language (VDL) -see [LW69] .
The task of formally describing the evolving PL/I language was separate from the language design team. Of course, there was strong interaction and communication. But, whenever the formalisation detected problems in the inherently ambiguous (and sometimes contradictory) natural language description, the formalists had to communicate the problem (sometimes by writing an indicative program). The response was then an amendment to the text which again might not be crystal clear.
Lesson: Separation of designers from formalists is far less productive than working as an interdisciplinary team.
Turning to key UK speakers to the 1964 working conference, both Christopher Strachey and Peter Landin spoke about a more abstract approach than operational semantics: rather than define an abstract interpreter, they were 5 John Backus made the initial proposal. 6 Peter Naur applied the notation to ALGOL and proposed extensions to the notation. 7 The proceedings of the conference [Ste66] took some time to be published but are invaluable to those who want to understand the development of ideas because the post-presentation discussions were captured.
proposing that the constructs of a programming language should be translated into mathematical functions. Such functions were written in a notation known as the Lambda calculus. The development of what later became known as denotational semantics, is a fascinating story of its own. Suffice it here to say here that researchers at Oxford University made the seminal contributions. 8 At the beginning of the 1970s, researchers at the IBM Lab in Vienna also made the step from operational to denotational semantics. The PL/I language was again a catalyst: the Lab had been invited to build the PL/I compiler for a radically new machine architecture. Unfortunately these machines were never built but the aspect of VDM (the Vienna Development Method) that related to describing language semantics was rescued by writing [BJ78, BJ82] . A more detailed account of this work can be found in [JA16, Ast19] and the step from VDL to VDM is discussed in [Jon01] .
Lesson Again there was a damaging wall between language designers 9 and the formalisers; moreover, the same mistake was repeated on a formal description of the machine architecture itself. In both cases the separation proved wasteful and far less effective than if there had been a more tightly knit structure.
Returning to the Baden-bei-Wien conference, Tony Hoare expressed unease about all of the proposed techniques because he saw the need to leave some aspects of a language undefined. Obvious cases include features of a programming language that relate to implementations on specific machines. But Hoare's interjection was prescient because concurrent programs can legitimately yield different results depending on the rate of progress of their separate threads. This observation led Hoare to develop an axiomatic approach [Hoa69] which is key to reasoning about programs satisfying formal specifications.
The challenge of describing -in an operational approach-concurrent programming languages with their inherent non-determinism was overcome by Gordon Plotkin's Structural Operational Semantics (SOS) [Plo81] . 10 The history of formal semantic descriptions is covered in a recent doctoral thesis [Ast19] and more technical details are given in [JA16, JA18] . Formalisation of the Spark-Ada language is discussed below in Section 4.
One obvious mode of transferring ideas from academic originators into industrial practice is for the originators to act as consultants to practitioners. This offers a way of overcoming the inevitable lack of knowledge of novel ideas in the receiving organisation but it runs several risks as outlined in the lessons spelled out at the end of this section. Specifically for formal methods ideas, this approach runs the risks associated with separation of practitioners from formalists mentioned in Section 2.
The largest of these engagements was the work at IBM on their CICS system (description below) but there are also some useful lessons from a less well known activity in STL that is covered in Section 4. The first issue is, of course, how to initiate the contact.
Before coming to CICS itself, some background activities are worth outlining. The aspects of VDM associated with the semantic description of programming languages are mentioned in Section 2 but VDM is more widely known as a development method for (general) programs. Early work on this aspect of VDM was actually undertaken inside IBM at the UK Laboratory in Hursley [Jon71, Jon73] ; the first book on this aspect of VDM was [Jon80] .
In the 1970s, there was a programme of European Laboratories Integrated Professional Training Program (ELIPT) technical courses. A course based on the 1980 VDM book was offered and taught by Derek Andrews and Cliff Jones. Management at the IBM Laboratory in Germany at Böbligen made the decision to enrol most of its active programmers on this course and employees attended in more-or-less coherent project groups. A typical course would begin at a hotel in the Schwarzwald with two weeks of lectures and writing exercises followed by a one week intensive workshop that initiated a formal description of a (simplified version of) the product of interest to that group of engineers. 11 (Managers claimed that they were too busy to commit to this length of course and a shorter Management Awareness course had to be prepared.) There were several significant success stories: one that is described in an external publication is [BHP83] .
In contrast to this organised enrolment, the IBM development laboratory in the UK at Hursley (Hampshire) simply let individuals from any project enrol on the ELIPT course in a fairly random way. This meant that when needed (see below) there was no critical mass of engineers who were all up to speed on VDM. The lesson here is that education needs to establish a cohort of people in the receiving organisation.
To emphasise this lesson it is worth comparing with Harlan Mills' success in IBM's Federal Systems Division (FSD). 12 Mills persuaded the director of FSD to attend the first course which ensured that no intermediate managers could claim they were too busy to take part. There was a notion of "passing" the course. Effectively, most development engineers in FSD attended.
Jones was by this time doing his belated Doctorate under supervision of Tony Hoare at Oxford University. Jean-Raymond Abrial arrived at the Programming Research Group at the same time (1979) as Jones. Hoare arranged that the two shared an office and many interesting discussions were conducted with Jones writing specifications in the VDM notation from [Jon80] and Abrial experimenting with what was to become the Z notation (see below).
CICS was IBM's Customer Information Control System which had evolved from a customer's 1968 program to be a full-blown IBM product that supported on-line transaction processing and was used by major financial and retail organisations. 13 In 1988 it consisted of well-over half a million lines of code in at least two languages. It was believed at one time to be one of IBM's most profitable program products.
Because of his contacts with IBM Hursley 14 and his on-going courses, Jones was asked about ways to help the CICS team adopt formal specification. Starting in 1980 there were informal discussions that led in early 1981 to the suggestion of a contract with a university (i.e. not with single consultants). Formal meetings between Hursley managers and Prof Hoare in the middle of 1981 resulted in a contract between IBM Hursley and Oxford University being in place by year end. Ib Sørensen and Tim Clement were to work on the project from the Oxford end; Hursley people included Pete Collins, John Wordsworth and Peter Lupton; Hoare had asked that Jones worked as a consultant on the project 15 and was joined by Rod Burstall of Edinburgh University in the same role.
As mentioned above, Abrial was developing the ideas that coalesced into the Z specification notation and it is clear that the challenges presented in describing CICS had an influence of this evolution. Key discussion partners also included Bernard Sufrin and Carroll Morgan. Ian Hayes joined the project in January 1983 which was perhaps the key time for the development of Z's so-called "schema calculus". Hayes also went on to edit the first book on Z [Hay87] . 16 Other Z books from around this time include [Spi88, Spi92, Wor92, MP93] and Mike Spivey also programmed the first tool that type-checked Z specifications.
A useful intermediate report on "CICS Experience with Z" is the (unrestricted) Technical Report [CNS87] . 17 The summary includes:
"From the industry point of view, this work has demonstrated that:
• provided that there is adequate education and support, a mathematical notation such as Z can be used for software development in an industrial environment;
• the use of formal methods changes the development process and brings greater precision to earlier stages;
• communication between development groups can be improved." • PRG staff funded by the collaborative contract had to spend significant amounts of time working on details of the CICS code;
• not only were general courses on Z designed and given to IBM engineers, but additional "readers' courses" were needed;
• the presence of "internal supporters" was crucial at the time of strongest interaction;
• there was a period when IBM engineers and management were pushing hard for a recognised standard for the Z notation; 19
• (and linked to the previous point) there was a perceived need for tools that helped creation, maintenance and analysis of Z documents; 20
• management support is crucial (see above on Mills and IBM FSD) -the attitude of IBM Hursley management ranged from supportive to antagonistic; 21
• King and Jones ascribe the drift away form the use of Z in Hursley down to people: there were probably not quite enough internal supporters, some moved on to other roles; less positive managers became responsible for decisions which affected the selection of methods to be used in later releases.
An extreme example of separation of both development from verification and the respective teams concerns the software for the Sizewell-B nuclear reactor. Sizewell-B was the first nuclear reactor in the UK to have a programmable primary protection system (PPS). The regulator (Nuclear Installations Inspectorate) decided that it was necessary for the PPS software to be formally verified. The software had been developed by the US company Westinghouse without a formal specification. It was written in PL/M-86 with some ASM86 and small amounts of PL/M-51 and ASM51; there were about 100,000 lines of unique executable code. Originally, there were two specification documents, a high level Software Design Requirements (SDR) and a more detailed Software Design Specification (SDS).
The chosen route to (partial) formal verification was to manually translate (in the UK) the SDR and SDS into a mathematical specification and to write a translator from PL/M-86 to IL, the Intermediate Language used as input to the MALPAS static analysis tool. This work started in January 1989 and completed in 1993. The MALPAS analysis project team grew to more than 80 and the project cost GBP 7 million. A review by Nuclear Electric [Fen95] concluded 19 An international standard for Z was approved in 2002. 20 Fuzz . . . 21 Jones' notes made at the time record one fairly senior manager responding to "it's just mathematical notation" with "I hate mathematics".
"The costs of the MALPAS review are high largely because the specification documents had to be manually translated into a formal notation before they could be used. This leads to the conclusion that the review processes need to be considered during the design phase of the project wherever possible". 22 This clearly reinforces the lessons that a separation of developers and formalists is damaging in general and that leaving verification to the late stages of development is both lengthy and difficult.
An extremely important vector of formal methods research and deployment centres around Jean-Raymond Abrial; this story links to the UK (and involvement of the current authors) but is actually more international. After laying the groundwork of what became the Z notation, Abrial returned to France and acted as an independent consultant. He not only made a fundamental shift to create the B-method [Abr96] 23 but he also developed a "B-tool" under contract to BP where Ib Sørensen had moved from Oxford after the CICS work. Subsequently, Abrial developed a completely new "Atelier-B" which was subsequently supported by the French formal methods companies ClearSy and Systerel. The notation and tool were used in the important development of the software of Metro line 14 for RATP [DM94] Abrial is a fascinating person who deserves a full biographical article. He is self-critical in the best possible way and has made several complete rethinks of his ideas. His next step was strongly influenced by books on Refinement Calculus by Carroll Morgan [Mor94] on the one hand and Ralph Back and Joakim von Wright [BvW98] on the other. Abrial's Event-B is described in [Abr10b] . Tool support was designed and built in an EU-funded project known as Rodin which was led by Newcastle University. The central tool activity was undertaken by Abrial, Laurent Voison and Steffan Hallerstede at ETH Zurich in the chair of David Basin. A subsequent EU-funded project (Deploy) 24 was again led by Newcastle and this time involved four industrial companies. As its name suggests, the emphasis here was on deployment of Event-B and the Rodin Tools. The most accessible description is [RT13] .
Although neither of the current authors were directly involved, it would be remiss in this section not to mention the work on hardware verification led by Mike Gordon of Cambridge -Larry Paulson wrote the Royal Society report [Pau18] . 25 Furthermore, the Oxford work on exploiting CSP by providing the FDR tool is to be described in a paper being written by Bill Roscoe.
This section considers the use of formal methods in some organisations that made them a more integral part of their development process.
Most if not all organisations that adopt formal methods will have progressed in stages of increasing rigour through informal and then structured methods, informed by their interactions with more advanced organisations and academics. One such organisation is the software engineering company Praxis (later Altran UK) founded by one of the authors of this paper (Thomas) with his colleague David Bean.
Thomas had worked on the design of a computer based PABX at Standard Telephones and Cables (STC) in north London in 1975/6 where he was involved in introducing and teaching functional decomposition using the diagrammatic Structured Analysis Design Technique, SADT [Ros77] . Bean had worked in a leading UK software house, Logica, and was familiar with Jackson Structured Programming (JSP) [Jac75] . They came together to set up the South West Universities Computer Centre (SWURCC) where Thomas recruited a small team to develop an Algol68 compiler that was required by SWURCC's user community to run on the ICL 2980 mainframe computer.
The Algol68 compiler used a front end, Algol68RS [WB83] developed at the Royal Signals and Radar Establishment (RSRE) in Malvern, UK by a team in the Mathematics Division that included Susan Bond, Ian Currie, John Morison and Philip Woodward. The Mathematics Division at RSRE ran the establishment computing service, having developed the UK's first solid-state computer and written its operating system and compilers. RSRE also developed cryptographic systems, formal static analysis tools to help identify trojan code and provably secure hardware systems (the VIPER processor), for example [Coh88] 26 using a formal hardware design and development system comprising the Electronic Logic Language (ELLA), developed by Morison and later released under a public license [MC93] supported by tools for design transformation, symbolic execution and formal verification. The SWURCC team impressed RSRE sufficiently that in addition to Algol68, they were commissioned to support and market ELLA.
SWURCC had built a reputation for software quality that led to them being invited to join a consortium (Augusta) funded by the UK Department of Trade and Industry to investigate the use of the new Ada programming language. Augusta was led by Tim Denvir of STC's telecommunications laboratory STL, who recalls that "Our report, delivered in September 1981, took a few example problems, expressed a design following several different methods, and developed implementations from each in Ada. We also did a literature study of many more design methods and of developers. Among the mostly structured methods (such as JSD) we used and/or considered CCS and VDM" [Den17] .
The SWURCC team became the kernel of Praxis, set up by Thomas and Bean in 1983, transferring the ELLA and Algol68 compiler support and other projects from SWURCC including a Unix re-implementation for ICL and a FORTRAN compiler for a military version of ICL's Distributed Array Processor.
Denvir (the rest of this paragraph draws heavily on Denvir, op. cit.) explains that STL had significant history in the use of Formal methods: by the mid 1970s they were already using Dijkstra's pre and post conditions to prove small programs correct. In January 1979, Denvir [Mil80] in revising the standard for the telecommunications industry standard design language SDL. 27 When the management changed at STC, Tim Denvir and Mel Jackson joined Praxis, bringing with them a European Commission contract to specify the Portable Common Tools Environment (PCTE) in an extended version of VDM (see [Mid89, Mid90] for VVSL). Praxis was a fertile environment for the introduction of formal methods. They abandoned SADT and adopted VDM [Jon80] and later Z [Spi89] as specification and design methods, particularly for safety or security critical projects such as the protection system for a radiotherapy machine, the certification authority to support the MONDEX smart card [HC02a], a system (SHOLIS) to support the landing of helicopters on naval ships [KHCP00] , and a system (CDIS) [Hal96] to support the UK National Air Traffic Services (NATS) controllers handling aircraft for the five London airports.
Static data flow and program analysis tools were developed at RSRE based on research by Bob Philips of RSRE. The work was declassified in the 1970s so that it could be used on civilian safety critical projects, resulting in two commercially available products, the Malvern Program Analysis Suite (MALPAS) and the Southampton Program Analysis Development Environment (SPADE, which became SPARK, see below) developed by a team led by Bernard Carré who were doing research in graph theory at Southampton University. Both MALPAS and SPARK have been used in the development and verification of a range of safety critical and security critical systems. SPADE was originally developed to analyse and verify programs written in a small subset of Pascal but Ada was then chosen as the foundation for future work. An Ada subset (the SPADE Ada Kernel or SPARK) was defined informally by Bernard Carré and Trevor Jennings in 1987 and more formally defined using a variant of Z in The Formal Semantics of SPARK [MO94] . Bernard Carré set up a company Program Validation Limited (PVL) and later sold it to Praxis, with the PVL staff becoming Praxis employees. SPARK has kept up with revisions of Ada as each has been standardised and some industrial applications have been described by Chapman and Schanda [CS14] . A survey of Praxis/Altran projects has been published by White, Matthews and Chapmen- [WMC17] . The Critical Systems Division of Praxis was acquired by Altran UK in 1997.
It is important to stress that the Praxis use of VDM, Z, CCS, and CSP was unusual if not unique. Most using formal methods used them to specify small, critical components; in Praxis these methods were used to specify system-level behaviour. This had a profound effect on the benefits and drawbacks that we found.
Some lessons from Praxis experience with formal methods:
• Praxis developed its own courses to teach its software engineers to use VDM and Z. The course lasted four days, preceded by a single day teaching discrete mathematics. This was found to be enough for computer science graduates to be able to read and start understanding a formal specification, though the ability to write good Z developed over a period of working on a project with access to experienced Z practitioners.
• formal methods had to be fitted into an overall development process and combined with other techniques, for example prototyping for user interfaces, and Data Flow Diagrams for process design. Further, no single formal method covers every aspect so Praxis had to use different techniques for functionality and concurrency and find ways of integrating these. They also had to write specifications at the system level and at the design level and show that the design was consistent with the system specification. Using high-level, set-theory based languages meant that there were almost no tools available which limited their ability to generate executable prototypes, or carry out proofs, model checking or automatic code generation.
• The benefits of this approach were a systematic, rigorous and traceable development leading to systems with few defects in service [Ame02, Sys06, HC02b, KHCP00] ; as Praxis improved their understanding of how to do this, they steadily drove down defect levels [HC02a, HC02c, Hal05] .
• Commercially, using formal methods had drawbacks as well as benefits:
-Customers were nervous about formal methods; the US National Security Agency asked Praxis to demonstrate the practicality of formal methods by developing an experimental system to control a secure enclave. The Tokeneer project was a success [BJW06] in that the NSA were unable to find any faults in the software, Praxis were able to train two NSA interns to extend the system, and the NSA said that the productivity of the Praxis team was the highest they had ever experienced but somehow this did not lead to sales of the SPARK toolset or to further NSA projects. The NSA later agreed that all of the Tokeneer specification, design and development could be publicly released including all the tools and proofs, 28 so that anyone could download and study the project, experiment with the proof technology and see whether other tools might reveal defects that had not been found. The various follow-on projects and experiments have been summarised in a book chapter by Jim Woodcock [WGC10] .
on the CDIS project for NATS, Praxis developed a formal VDM specification during the bid, to determine exactly what the customer meant by their requirements. This led to over 100 requests to NATS for clarifications but it enabled Praxis to feel comfortable bidding for a large project whose cost exceeded Praxis' annual turnover 29 and to contract to repair at no charge any major faults that developed over the following five years. NATS later said that CDIS had been by far the easiest system to integrate that they had experienced and its stability was so good that they had to ask Praxis after a few years to retrain their staff in how to restart CDIS because it had failed so rarely that they were unsure how to do it.
-The functional specification for CDIS and subsystem specifications for the two component parts (server and workstation) were expressed in VVSL but the user interface used state transition diagrams and, for modelling concurrency used CSP and for the LAN design used Milner's CCS. Praxis' technical architect, Anthony Hall, has described and explained the choice of methods [Hal96] . With NATS agreement, Praxis made the CDIS code and project records available for analysis by two academic researchers. Their conclusions [PH97] were that formal methods can contribute to achieving very reliable code (but with many reservations, for which see the cited paper).
-Formal methods projects of this sort need considerable work before any benefits are seen, which made it difficult to convince potential customers to invest in such projects.
-The lack of support tools can be a major problem for the use of formal methods that only address the specification stage. Some form of prototyping is very important so that clients can validate the specification and request changes while it is still relatively inexpensive to change it.
-System specifications need to be understood by domain experts as well as by computer scientists. Praxis rewrote the informal specifications using and including the formal specification so that it could be understood by clients. Preparing a formal specification facilitates writing a better structured, clearer and shorter specification in natural language.
28 https://www.adacore.com/tokeneer. 29 Thomas remarked to Jones over a dinner in Brussels that he had "bet the company on VDM".
-Praxis offered some free warranties for projects that had a formal specification agreed with the client, as this made it possible to distinguish between errors and specification changes. This was less commercially risky than it might seem, because the warranty would be voided if the client changed the software themselves or asked another company to implement new features.
-NATS subsequently contracted Altran UK to develop a new ATC system iFACTS 30 that was successfully delivered using Z and SPARK.
Thomas was present at one NATS meeting before this contract was awarded where the objection was raised that if NATS presented their regulator (The UK Civil Aviation Authority) with SPARK code and formal proofs as part of the evidence for the safety of iFACTS, there was a risk that the CAA would always require such strong evidence in future!
Apart from the lessons for those wishing to deploy formal methods, there are exogenous factors that have affected the growth and adoption of formal methods. This section covers some of these influences.
In the UK, funding from its research councils has been supportive to both the underlying research and deployment of formal methods. In fact, it can be argued that such funding was pivotal in the 1970s: 31 viewed from Manchester University (where Jones was at that time) it facilitated the creation of a world class formal methods activity. It is also worth noting that BP's "Future ventures" programme provided funding for activities in Edinburgh Univerity's Laboratory for Foundations of Computer Science (and for Edsger Dijkstra).
The body principally responsible for funding computer science research in U.K. Universities was then known as SERC. The Computer Science committee, recognising the importance of distributed computing as a research area, (1981-1984) . The primary scientific objectives of the programme were to seek an understanding of the principles of Distributed Computing Systems and to establish the engineering techniques necessary to implement such systems efficiently. These broad objectives reflect the relative immaturity of the subject when the programme was founded. In particular the programme sought to establish an understanding of parallelism in information processing systems and to devise ways to take advantage of this. When the DCS programme was first established, the research covered five major topic areas, representing a progression from fundamental theory to novel applications. The areas were:
• Theory and Languages: An adequate theoretical basis for Distributed Computing Systems.
• Resource Management: Distribution of control, allocation, scheduling and organization.
• Architecture.
• Operational Attributes: Particularly reliability and performance.
• Design, Implementation and Application: Hardware and software techniques for development and implementation.
A major theme in DCS was concerned with theories of parallel computation and with the development of notations and techniques for specifying and verifying such systems. 32 The UK Alvey Programme ran from 1983-87 and also invested in formal methods. 33 The focus of the Alvey programme [OO90] was pre-competitive advanced information technology research. It comprised four areas that seemed particularly relevant at the time:
• Software Engineering (led by David Talbot from ICL with Rob Witty from Informatics as his Deputy, who brought the focus on formal methods from DCS).
• Intelligent Knowledge Based Systems
• Advanced Microelectronics (VLSI Design)
Research was a collaboration between academia, government and industry; it was directed into important areas and coordinated and the funding was substantial, GBP 350M at 1982 prices. The Programme put together 210 projects lasting on average 3 years and involving 2500 people at its peak.
The largest Alvey project in Software Engineering funded Manchester University and ICL 34 to construct an integrated project support environment dubbed IPSE 2.5. Researchers at Manchester and EPSRC's own Rutherford Lab delivered a theorem proving assistant Mural [JJLM91] which was licensed to Winfrith Atomic Energy Establishment.
Another activity under the Alvey programme led to the creation of a handbook of formal methods. The contents attempted to identify areas of applicability for notations such as VDM, Z, CSP and CCS.
Cliff says: I hope to find some trace of this when, post-Covid, I can get back into the university! As recently as the 2010s, formal methods was still identified as an area for growth of EPSRC funding.
Funding from the various European Union research framework programmes has also been a significant aid to formal methods research and deployment. Again focussing on items where the authors have first-hand knowledge, one of the longest-lasting impacts started with funding of an activity called VDM-Europe: meetings in Brussels of experts were supported for several years and led to the first symposium of VDM-Europe [BJMN87] . These conferences morphed 35 into FM-E which not only organises a highly-rated symposium at roughly 18-monthly intervals but has also held two World Congresses [WWD99, tBMO19] and has widened its venues to North America, Singapore (and the 2021 event is planned for China). 36
The question of how much the adoption of formal methods is influenced by the availability of tool support is interesting but is not universally agreed. Early on, large formal descriptions were constructed with minimal tool support. A significant example is the formal description of PL/I from the IBM Vienna Lab. It is probably fair to say that the risks of introducing inconsistencies are far higher when a document is revised than when it is first constructed. It is however clearly short-sighted not to at least syntax and type check and large block of formulae.
The question is how much further one can go without the tool support becoming an end in itself and possibly even distracting from the thought process that is crucial to the construction of an abstract model. Jim Horning (private communication) captured one of the reservations about tools with his phrase 34 This project came close to non-submission when, having crafted a neat collaboration of three industrial organisations (STL, IDEC and ICL), Jones was informed that they were merging and that the combination of their individual intended commitments was not defensible to a single board of directors. Brian Warboys then of ICL steered a tense period of revisions at the eleventh hour.
35 Jim Woodcock tackled Jones about widening the remit of VDM-Europe to include other specification languages. 36 see http://www.fmeurope.org/ "mental versus metal tools". At least some of the differences in people's evaluation of the role of tools can be accounted for by the contribution they hope to result from using formalism. It is relatively easy to persuade organisations to use tools that analyse finished code in order to detect potential errors. There are sub-issues here: Peter O'Hearn (see Section 6.1) points out the tools that detect too many false positives are unlikely to endear themselves to developers. But, broadly, using model-checking tools in a development process that does not require deep understanding from the developers of formal methods is an easier sell than starting out by insisting that developers must employ formalism in the specification and early design phases.
The authors of the current paper however both argue that the real payoff of formal methods comes from their use early in the design phase. Thomas has written [Tho93] about the cost-effectiveness of using formal methods early; the Tokeneer study mentioned in Section 4 supports this view; Figure 1 provides evidence that formalism used to front-load thinking pays off; a similar result can be seen in the dual-track study reported in [BFL96] .
Many companies are willing to buy tools as they see this as a quick fix but fail to recognise that tools exist to support methods and the main investment has to be in adopting the methods.
The view of "mental tools" in no way removes the need for tool support but it does moderate the extent to which the tool can be allowed to become the master of the method. For example, a large formal text might be regarded as an obvious input to a theorem proving system. Unfortunately, there are few success stories of such efforts. 37 The reason would appear to be that theorem proving systems not only require learning another formalism but that their modes of interaction distract from thinking about the application in hand. There are numerous stories of formal machine-checked proofs that do not actually capture what the user intended to establish.
Examples of tools that offer fairly direct support for established specification languages include a VDM tool from Adelard, 38 the IFAD Toolset (also for VDM) that has subsequently been developed into an open-source Overture tool. Probably the most significant set of tools come from Abrial with the Rodin tool support 39 for Event-B being the most recent.
One way in which the use of formalism could be encouraged is via standards. In May 1989 the UK Ministry of Defence (MoD) issued Interim Defence Standard 0055 Requirements for the procurement of safety critical software in defence equipment for comment. The interim standard required that safety critical 37 The US work starting with the Boyer-Moore prover through to ACL/2 is a notable achievement -see [Moo19] . 38 The work of the Adelard company would justify a paper of its own. for example their development of the "Dust Expert" software is reported in [CCFJ99] .
39 See http://www.event-b.org/ software should be formally specified and formally verified. Several companies in the defence industry attempted to persuade the MoD to withdraw the interim standard; but the MoD issued it as an interim standard in 1991 and made the standard mandatory for the SHOLIS project [KHCP00] . The interim standard was replaced by a full version in 1997, 40 retaining the requirements for formal methods and including several examples from the SHOLIS project. Def Stan 00-55 issue 3 recommended the use of civil standards such as RTSA DO-178, ISO 61508 and RTSA DO-254. IEC 61508 is the international standard for functional safety of programmable electronic systems. It requires that each safety function has a Safety integrity Level that defines the allowable probability of failure: for continuous control of the most safety critical function (SIL4) the allowable probability must not exceed 10 −8 /hour. The standard recommends the use of formal methods for a SIL4 software safety function but does not mandate their use. In successive revisions of the standard, major European companies have repeatedly frustrated attempts to make formal methods mandatory for SIL 4 software.
Returning to Harlan Mills and what he achieved in IBM's Federal Systems Division (and again relying on Jones' memory of personal discussions with Mills) perhaps he had the best approach to standards. At one point in time, a standard for software developers stated that programmers should accompany loops with an indication of why they were claimed to achieve their aim; there was not a mandated style for such annotations but the document did offer an example of a style that would serve.
There is of course also the question of standards for the formalism itself. It was mentioned in Section 3 that, during the CICS effort, there was a request from IBM for a standard for the Z notation itself. This is an understandable wish in that it opens up the possibility of sourcing tools and expertise from different organisations. In fact, VDM was in 1996 the first formal method notation to get an ISO standard 41 the Z standard followed in 2002. 42
Our emphasis in this paper has been on lessons that can be derived from early attempts to apply research on formal methods in significant software development. This should in no way be seen as expressing reservations about the potential of the ideas and Section 6.1 points to two important recent success stories. If we cannot learn from earlier difficulties, no progress is made. Rather than re-list all of the lessons noted earlier in the paper, Section 6.2 pinpoints a few key messages. [DFLO19] ) that are used in the standard development cycle by Facebook engineers. In a private conversation with Jones, O'Hearn attributed the positive adoption by practicing engineers both to the creation of apposite tools and the fact that the the general knowledge of fundamental computer science ideas is much more widespread now than in the attempts reported on earlier in this paper that mainly date from the last century.
Byron Cook's [Coo18] is one of a sequence of papers reporting on application of formal methods at AWS; his recorded keynote 43 talk at FLoC-18 in Oxford is inspirational and, related to the lessons about management commitment, even more impressive are the talks from senior managers at AWS. 44
The contributions of UK researchers to the fundamental ideas that have shown how formal concepts and notations can be used in the description and and development of software are significant. Rather than list and attribute the scientific source material, we have in this paper identified some significant attempts to deploy the theory into practical environments. As indicated at the beginning of the paper, we have mainly reported on deployments of which we have first hand knowledge. These close encounters have made it possible to analyse the difficulties that were experienced.
Probably the most important single difficulty that complicated early deployments was the relatively small number of people available in receiving organisations who had acquaintance with a broad knowledge of theoretical concepts. A short course on one or another specific notation does not equip someone to apply that notation to abstract away from the details of potential implementations; similarly, nor does being shown a few examples of proofs convey the fundamental idea of recording a convincing correctness argument. The more recent experiences from major companies like Microsoft, Amazon and Facebook suggest that the general educational environment now provides a far better basis than was available last century.
The attitude and commitment of management is clearly related and also of major importance. The graph in Figure 1 indicates a challenge for managers who only feel comfortable when they can "weigh the code": just as in all engineering endeavours, care and thought early in development clearly pays off later but the early effort does not yield lines of code. (Nor does the drawing of careful architectural plans lay any bricks.)
Linking the points about technical expertise and management commitment is the issue of whether the key expertise is inside the receiving organisation or supplied by external consultants. Key advantages that come from the research expertise being within the deployment organisation are bandwidth of communication and stability. Perhaps more important is the avoidance of a split between "practical" work and post hoc formalisation. This division appears to have been a source of problems in many of the early attempts to gain benefit from using formal methods.
Another issue is the choice of project -perhaps crucially the first project. A significant success story that lays about as far from our stated geographic focus as can be is the work in Australia at CSIRO Data61 (previously known as NICTA). Gerwin Klein and his team recognised the importance of microkernels because weaknesses here open any software built on top of them to subversion. A recent papers on sel4 is [HKA20] and earlier publications can be traced from its references. In today's world where almost everything depends on software, it is sometimes a financial aspect that identifies a development as "business critical". There is, of course, the class of "safety critical" systems that comprised early deployments of formal methods. What the sel4 exercise is a reminder of is that underlying software can provide a Trojan Horse on which reliance should only be proportional to its demonstrated trustworthiness.
One closing (and perhaps uncomfortable for the current authors) lesson was mentioned by Jonathan Lawrence when he kindly reviewed the lessons from the IBM CICS project: he suggested that one should "not to be too ambitious". It would be legitimate to ask whether some of the early deployments withered on the vine precisely because researchers wanted to see the full extent of their research put into practice even if the receiving organisation was unready.