Verification of picture generated code

Tools such as Simulink(R) are being used by engineers around the world to model and solve real problems about dynamical systems. In particular control systems are modelled graphically, simulated and then code is generated automatically. Code generated from such a tool is being proposed for use in safety critical control systems. The problem for certifiers is why should they trust such generated code? This paper describes a particular approach to solving this problem which supports review by a certifier. A small case study is presented to illustrate the approach and the technical issues involved