Correctness by construction: Integrating formality into a commercial development process

Abstract

This paper describes a successful project where we used formal methods as an integral part of the development process for a system intended to meet ITSEC E6 requirements. The system runs on commercially available hardware and uses common COTS software. We found that using formal methods in this way gave benefits in accuracy and testability of the software, reduced the number of errors in the delivered product and was a cost-effective way of developing high integrity software. Our experience contradicts the belief that formal methods are impractical, or that they should be treated as an overhead activity, outside the main stream of development. The paper explains how formal methods were used and what their benefits were. It shows how formality was integrated into the process. It discusses the use of different formal techniques appropriate for different aspects of the design and the integration of formal with non-formal methods.