The Evolution of Def Stan 00-55 and 00-56: An Intensification of the ‘Formal Methods Debate’ in the UK

Abstract

This paper traces the evolution of two standards regulating the identification and production of safety-critical software for defence applications, issued by the Ministry of Defence as Interim standards in 1991. Def Stan 00-55 governs The Procurement of Safety-Critical Software in Defence Equipment and Def Stan 00-56 governs Hazard Analysis and Safety Classification of the Computer and Programmable Electronic System Elements of Defence Equipment. The standards - 00-55, in particular - have become an important forum for articulating the fears and aspirations of those who work in the UK safety-critical software engineering field - one which has largely revolved around the integral role 00-55 demands for formal methods of software development for safety-critical functions or components. In recounting the story of their gestation within the MoD during the early '80s; their controversial release in draft form in 1989; and their subsequent second release as interim standards in 1991, the object has been to illuminate some of the current 'politics' of formal methods of software production, and to consider how the standards gel - or jar - with an emergent sense of the place of formal methods within the discipline of software engineering.