Struggling to Be Accepted: The Early Industrial Life of Formal-Methods Technology

In 1990, the semiconductor company Inmos and Oxford University Computing Laboratory were jointly conferred the prestigious Queen's Award for Technological Achievement. This resulted from their innovative development and use of formal methods on the verification of the T800 - the second generation of the British microprocessor known as the transputer. The Queen's Award coronated formal methods with an image of unquestionable success. The technology had proven to be an important tool in the design of the T800 and the Award symbolized what looked like their definite establishment within the Inmos' design process. But how much was this perception shared within the company? Was the emergence of formal methods within Inmos' design process such a happy event as the news seemed to imply? Did formal methods really gain an unquestionable place within the company's design process? This paper looks closely at the T800 experience of formal methods with a view to answering these questions. More generally, it seeks to cast light on the subtlety of the interactions between existing and emerging technical traditions in the design process. Ultimately, it seeks to cast light on the behavioural nature of the processes whereby emerging technologies do, or do not, become established as valuable ingredients in the life of a company. The paper contains a brief presentation of behavioural concepts relevant to the case-study; a review of relevant factors influencing the present general development of formal methods; and an analysis of the experience of the T800 FPU and its subsequent impact for the establishment of formal methods within the Inmos' design process. The analysis is informed by the concept of sociotechnical constituencies.