Proving correctness of autocoded control software

Fernando Alegre, Rene C. Valenzuela, Eric Feron, Santosh Pande

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish (US)
Title of host publicationCollection of Technical Papers - 2007 AIAA Modeling and Simulation Technologies Conference
PublisherAmerican Institute of Aeronautics and Astronautics
Number of pages15
ISBN (Print)1563479060
StatePublished - Jan 1 2007
Externally publishedYes


Dive into the research topics of 'Proving correctness of autocoded control software'. Together they form a unique fingerprint.

Cite this