Qualification of automatic code generation using formal techniques

The slow industrial take-up of formal methods is partly due to their high cost when considered on a per-system basis. Formal methods are best employed either on relatively small and strictly bounded sub-problems within a project, or on the qualification of components and tools that are used on successive projects. One class of tools that are becoming more commonly used are graphical specification editors that provide an automatic code generation facility. There are a number of advantages that arise if such tools are used for production quality code. Not least of these is the potential for reducing the risk and cost of software development, by reducing the potential for the introduction of errors, and increasing the speed with which software can be produced. The magnitude of these advantages is increased where the risk and cost of software production is higher, such as in the case of high-integrity systems development. In order to derive these benefits, it is vitally important to ensure that the generated code is functionally faithful to its specification. The British Aerospace Dependable Computing Systems Centre is looking at how formal techniques can be employed to ensure that an automatic code generator produces code that is faithful to its specification. The use of formal techniques is important to this process, since it is only through these that the high level of assurance required can be attained. (2 pages)