Proving correctness of autocoded control software

We show a methodology to automate the verification of safety properties of control systems software generated by an autocoder. The verification algorithm, due to Feron, transforms an initial proof provided at the modeling level into the corresponding proof at the implementation level. It is based on a series of affine transformations of ellipsoid invariants induced by the statements in the target source code. We use source-to-source code transformations to reshape the autocoded source into a form suitable for application of our algorithm. In particular, we use Simulink and its Real Time Workshop for model design and the CIL/BLAST program analyzers as the basis for our verification framework. Preliminary results show that this approach is a very inexpensive way to guarantee safety without imposing much burden on system designers, because it requires them to provide, via a high-level language like that used for modeling, just the key information about the model that makes the automated proof successful.