Model-based design and automated code generation are being used increasingly at NASA. Many NASA projects now use MathWorks Simulink and Real-Time Workshop for at least some of their modeling and 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 generators 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. Indeed, manual review of autocode can be more challenging than for hand-written code. Since the direct V&V of code generators is too laborious and complicated due to their complex (and often proprietary) nature, we have developed a generator plug-in to support the subsequent certification of the code that is generated. Specifically, the AutoCert tool supports 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 enables missions to obtain assurance about the safety and reliability of the code without excessive manual V&V effort and, as a consequence, increases the acceptance of code generators in safety-critical contexts.
A Software Safety Certification Tool for Automatically Generated Guidance, Navigation and Control Code
2008-03-01
627803 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Building Heterogeneous Safety Cases for Automatically Generated Code
British Library Conference Proceedings | 2011
|Safety Critical Systems Certification: Tool Qualification for Hardware and Software
British Library Conference Proceedings | 2010
|