An Approach to Automatic Code Generation for Safety-Critical Systems

Abstract

Although formal requirements specifications can provide rigorous and unambiguous description of a safety-critical software system, designing and developing production quality code from high-level specifications can 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.

In this report we outline the requirements of such code generation to obtain a high level of confidence in the correctness of the translation process. We then describe a translator for a state-based modeling language called RSML that largely meets these requirements. The process is based on the denotational semantics of both RSML and a simplified imperative target language (SIMPL), which are used to prove that the translator correctly implements the RSML semantics in SIMPL. The SIMPL code can then trivially be translated to any popular imperative language. The translation process also provides for informal arguments of the correctness of the code and traceability information.