Natural Language Interface for Safety Certification of Safety-Critical Software

Ames Research Center, Moffett Field, California

Model-based design and automated code generation are being used increasingly at NASA. 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.

The AutoCert generator plug-in supports the certification of automatically generated code 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 effort. The key technical idea is to exploit the idiomatic nature of auto-generated code in order to automatically infer logical annotations that describe properties of the code. These allow the automatic formal verification of the safety properties without requiring access to the internals of the code generator. The approach is therefore independent of the particular generator used. The use of a combined generation/analysis tool can allow system engineers to concentrate on the modeling and design, rather than worrying about low-level software details. By providing tracing between code and verification artifacts, and customizable safety reports, the tool supports both certification and debugging. Although integrated with the code generator, AutoCert is functionally independent in the sense that it does not rely on the correctness of any generator components. The tool has two main benefits: (1) it helps catch bugs in autocoders, and (2) it helps with the certification process for the autogenerated code, thus mitigating the risk of using COTS autocoders that lack a trusted heritage.

The AutoCert technology also has a number of advantages over other approaches to formal verification. It can handle code with arbitrary loops, and can handle code generated from both continuous and discrete models. Moreover, the certification system based on annotation inference is more flexible and extensible than decentralized architectures where certification information is distributed throughout the code generator. Identifying the patterns that are used to infer the annotations is an iterative process, but by allowing tracing between VCs (verification conditions) and statements of the auto-generated code, the tool lets missing annotations and, thus, missing patterns, to be pinpointed more easily. By raising the level of abstraction at which verification knowledge is expressed, one can concisely capture many variations of the underlying code idioms. In particular, one can easily deal with optimizations that obscure low-level code structure.

This program was written by Ewen Denney and Bernd Fischer of USRA/RIACS for Ames Research Center. For more information, download the Technical Support Package (free white paper) at www.techbriefs.com/tsp under the Software category.

Inquiries concerning rights for the commercial use of this invention should be addressed to