Formal methods light: experience applying formal specification in the aerospace and nuclear sectors

The article describes two industrial projects in which formal methods were applied in the early stages of system development. Both projects were based on the selective application of formal methods, with appropriate techniques targeted on those areas of development where they would be expected to yield a benefit. We term this approach “formal methods light” to contrast with the rigorous application of formal modelling and analysis at all stages in the development of a computing system. The projects discussed are: 1. The BASE Trusted Gateway-British Aerospace (Systems and Equipment) Ltd. developed a secure message handling system, using formal modelling to describe the system´s security policy and its functionality. Here formal techniques were used to help understand requirements and represent designs. 2. The BNFL Tracking Manager-BNFL Engineering and Manchester University used formal modelling to analyse the safety properties of a proposed new architecture for systems to track the movement of nuclear materials through industrial processing. Here formal techniques were to assist in the analysis of a proposed architecture rather than as the first stage in software development