Auto-coding/auto-proving flight control software

This work describes the results of an experiment to compare conventional software development with software development using automatic code generation from Simulink and mathematically based code verification (proof). A real industrial scale, safety critical system was used as the basis for the experiment in order to validate results, although this imposed some constraints. The principal aims for the experiment were to answer the following three questions. 1. Could automatic code generation be integrated with the verification tools to give a software development process to produce software that would pass the existing functional unit tests? 2. Would the code be of sufficient quality to be flown, i.e. was it certifiable? 3. What were the cost implications of adopting the process as part of a development lifecycle? The experiment showed how to integrate the techniques into existing development processes and indicated where processes could be streamlined. The code and the technique were independently assessed as being certifiable for safety critical applications. The results of the experiment were generally positive indicating the potential for reductions of 60%-70% of the software development costs alone, that would translate into a 30%-40% reduction in software life cycle costs.