Table of Contents
Fetching ...

The development and deployment of formal methods in the UK

Cliff B. Jones, Martyn Thomas

TL;DR

This article lists key ideas and indicates where attempts were made to use the ideas in practice and an attempt is made to tease out lessons that influence the probability of successful long-term changes to software engineering.

Abstract

UK researchers have made major contributions to the technical ideas underpinning formal approaches to the specification and development of computer systems. Perhaps as a consequence of this, some of the significant attempts to deploy theoretical ideas into practical environments have taken place in the UK. The authors of this paper have been involved in formal methods for many years and both have tracked a significant proportion of the whole story. This paper both lists key ideas and indicates where attempts were made to use the ideas in practice. Not all of these deployment stories have been a complete success and an attempt is made to tease out lessons that influence the probability of long-term impact.

The development and deployment of formal methods in the UK

TL;DR

This article lists key ideas and indicates where attempts were made to use the ideas in practice and an attempt is made to tease out lessons that influence the probability of successful long-term changes to software engineering.

Abstract

UK researchers have made major contributions to the technical ideas underpinning formal approaches to the specification and development of computer systems. Perhaps as a consequence of this, some of the significant attempts to deploy theoretical ideas into practical environments have taken place in the UK. The authors of this paper have been involved in formal methods for many years and both have tracked a significant proportion of the whole story. This paper both lists key ideas and indicates where attempts were made to use the ideas in practice. Not all of these deployment stories have been a complete success and an attempt is made to tease out lessons that influence the probability of long-term impact.

Paper Structure

This paper contains 10 sections, 1 figure.

Figures (1)

  • Figure 1: Figure reproduced from HoustonKing indicating errors found at different development stages. [Original caption] Comparison of problems found with two development methods for CICS/ESA V3.1