Model-based design and automated code generation are being used increasingly at NASA. By some estimates, 50% of all NASA projects now use MathWorks Simulink and Real-Time Workshop for at least some of their code development. The trend is to move beyond simulation and prototyping to actual flight code, particularly in the Guidance, Navigation, and Control domain. However, there are substantial obstacles to more widespread adoption of code generators in such safety-critical domains. Since code genera-tors are typically not qualified, there is no guarantee that their output is correct, and consequently the generated code still needs to be fully tested and certified. Moreover, the regeneration of code can require complete recertification, which offsets many of the advantages of using a generator.

Since the direct V&V of code generators is too laborious and complicated due to their complex (and often proprietary) nature, we instead propose a generator plug-in to support the subsequent certification of the code they generate. Specifically, our tool will support certification by formally verifying that the generated code is free of different safety violations, by constructing an independently verifiable certificate, and by explaining its analysis in a textual form suitable for code reviews. This will enable missions to obtain assurance about the safety and reliability of the code without excessive manual V&V effort and, as a consequence, increase the acceptance of code generators in safety-critical contexts. The generation of explicit certificates is particularly well-suited to supporting independent V&V. The key technical idea of our approach is to exploit the idiomatic nature of auto-generated code in order to automatically infer logical annotations. These allow the automatic formal verification of the safety properties without requiring access to the internals of the code generator. Hence, the approach is independent of the particular generator used. We will demonstrate the feasibility of our approach on helicopter flight code from NASA's RASCAL project that has been generated using MathWorks Real-Time Workshop (RTW), an automatic code generator that translates from Stateflow/Simulink models into embedded C code.