Colloquium Details
Assurance Techniques for Code Generators
| Author: | Bernd Fischer University of Southampton |
|---|---|
| Date: | October 20, 2006 |
| Time: | 11:00 - please note special day and time |
| Location: | 220 Deschutes |
| Host: | Yannis Smaragdakis |
Abstract
Automated code generation is an enabling technology for model-based software development and promises many advantages but the reliability of the generated code is still often considered as a weak point, particularly in safety-critical domains. Traditionally, correctness-by-construction techniques have been seen as the "right" way to assure reliability, but these techniques remain difficult to implement and to scale up, and have not seen widespread use. Currently, generators are validated primarily by testing, which cannot guarantee reliability and quickly becomes excessive. In this talk, we present two related alternative assurance approaches that use Hoare-style safety proofs to ensure that the generated code does not "go wrong", i.e., does not violate specific safety conditions during its execution.
The first approach is based on the insight that code generator itself can be extended to produce all annotations (i.e., pre-/postconditions and loop invariants) required to enable the safety proofs for each individual generated program, without compromising the assurance provided by the subsequent verification phase. This is achieved by embedding annotation templates into the code templates, which are then instantiated in parallel by the generator. This is feasible because the structure of the generated code and the possible safety properties are known when the generator is developed. It does not compromise the provided assurance because the annotations only serve as auxiliary lemmas and errors in the annotation templates ultimately lead to unprovable safety obligations. We have implemented this approach in the AutoBayes and AutoFilter code generators and used it to fully automatically prove that the generated code satisfies both language-specific properties such as array-bounds safety or proper variable initialization-before-use and domain-specific properties such as vector normalization, matrix symmetry, or correct sensor input usage.
The second approach is based on the insight that the output of a code generator is highly idiomatic, so that we can use patterns to describe all code constructs that require annotations and templates to describe the required annotations. We use techniques similar to aspect-oriented programming to add the annotations to the generated code: the patterns correspond to (static) point-cut descriptors, while the introduced annotations correspond to advice. The resulting annotation inference algorithm is generic with respect to the safety property and can run completely separately from the generator, which can thus be treated as a black box. This allows us to apply it to to third-party generators like RealTime Workshop as well.