Trustworthy translation for the Requirements State Machine Language without Events

Although formal requirements specifications can provide a complete and consistent description of a safety-critical software system; designing and developing production quality code from high-level specifications can still be a time-consuming and error-prone process. Automated translation, or code generation, of the specification to production code can alleviate many of the problems associated with design and implementation. However, current approaches have been unsuitable for safety-critical environments because they employ complex and/or ad-hoc methods for translation.; This dissertation discusses the issues involved in automatic code generation for high-assurance systems. It first defines a set of requirements that code generators for this domain must satisfy, then describes a translation from the Requirements State Machine Language without Events (RSML-e ) to a simplified imperative language (SIMPL) that satisfies these requirements. Both the evaluation semantics and transformations of the source and target languages are specified using extended natural semantics rules. The central work of the thesis is in two parts: first, a complete formalization of the RSML-e language, and second, a proof that the translation preserves the behavior of the original specification. The primary novelty is in using higher-order abstract syntax and extended natural semantics for the transformations. This choice significantly simplifies the proof effort and utilizes a different reasoning style than first-order natural semantics proofs.