On the requirements of highintegrity code generation

Although formal requirements specifications can pro-vide a complete and consistent description of a safety-critical software system, designing and developing produc-tion quality code from high-level specifications can be a time-consuming and error-prone process. Automated trans-lation, or code generation, of the specification to produc-tion code can alleviate many of the problems associated with design and implementation. However, current ap-proaches have been unsuitable for safety-critical environ-ments because they employ complex and/or ad-hoc methods for translation. In this paper, we discuss the issues involved in automatic code generation for high-assurance systems and define a set of requirements that code generators for this domain must satisfy. These requirements cover the formality of the trans-lation, the quality of the code generator, and the properties of the generated code.