Automating traceability for generated software artifacts

摘要

Program synthesis automatically derives programs from specifications of their behavior. At a lower level, compilation automatically derives machine code from source code (i.e. from a specification of its behavior). An advantage of program synthesis/compilation, as opposed to manual coding, is that there is a direct link between the specification and the derived program. This link is, however, not very fine-grained: it can be best characterized as program is-derived-from specification. When the generated program needs to be understood or modified, more fine-grained linking is useful. We present a technique for automatically deriving traceability relations between parts of a specification and parts of the synthesized program. The technique is very lightweight and we expect it to work - with varying degrees of success - for any process in which one artifact is automatically derived from another. We illustrate the generality of the technique by applying it to two kinds of automatic generation: synthesis of Kalman filter programs from specifications using the AUTOFILTER program synthesis system, and generation of assembly language programs from C source code using the GCC C compiler. We evaluate the effectiveness of the technique in the latter application.